no goals
R : Type u_1
V : Type u_2
V' : Type ?u.504435
P : Type u_3
P' : Type ?u.504441
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ Wbtw R x y z ↔ z = y ∨ x ∈ ↑(lineMap z y) '' Set.Ici 1
rw [wbtw_comm, wbtw_iff_left_eq_or_right_mem_image_Ici]