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)
: