let AS be AffinSpace; :: thesis: for a, b being Element of AS
for A being Subset of AS st A is being_line & a in A holds
( b in A iff a,b // A )
let a, b be Element of AS; :: thesis: for A being Subset of AS st A is being_line & a in A holds
( b in A iff a,b // A )
let A be Subset of AS; :: thesis: ( A is being_line & a in A implies ( b in A iff a,b // A ) )
assume that
A1: A is being_line and
A2: a in A ; :: thesis: ( b in A iff a,b // A )
consider p, q being Element of AS such that
A3: p <> q and
A4: A = Line (p,q) by A1;

hereby :: thesis: ( a,b // A implies b in A )

assume b in A ; :: thesis: a,b // A
then p,q // a,b by A2, A3, A4, Th21;
then a,b // p,q by Th3;
hence a,b // A by A3, A4; :: thesis: verum

end;

assume a,b // A ; :: thesis: b in A
then consider p, q being Element of AS such that
A5: p <> q and
A6: A = Line (p,q) and
A7: a,b // p,q ;
p,q // a,b by A7, Th3;
hence b in A by A2, A5, A6, Th21; :: thesis: verum