no goals
R : Type u_1
V : Type u_2
V' : Type ?u.511588
P : Type u_3
P' : Type ?u.511594
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ Sbtw R x y z ↔ z ≠ y ∧ x ∈ ↑(lineMap z y) '' Set.Ioi 1
rw [sbtw_comm, sbtw_iff_left_ne_and_right_mem_image_Ioi]