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, 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, A3, A4, Th36;
then a,b // p,q by Th13;
hence a,b // A by A3, A4, Def4; :: 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 by Def4;
p,q // a,b by A7, Th13;
hence b in A by A2, A5, A6, Th36; :: thesis: verum