theorem AffineSubspace.mem_of_collinear {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {x y z : P} (h : Collinear k {x, y, z}) (hx : x ∈ s) (hz : z ∈ s) : y ∈ s