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
A4: p <> q and
A5: A = Line (p,q) by A1, Def3;

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

assume b in A ; :: thesis: a,b // A
then p,q // a,b by A2, A4, A5, Th36;
then a,b // p,q by Th13;
hence a,b // A by A4, A5, Def4; :: thesis: verum

end;

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