let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS
for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds
( a,b // A iff a,b // c,d )
let a, b, c, d be Element of AS; :: thesis: for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds
( a,b // A iff a,b // c,d )
let A be Subset of AS; :: thesis: ( c in A & d in A & A is being_line & c <> d implies ( a,b // A iff a,b // c,d ) )
assume that
A1: c in A and
A2: d in A and
A3: A is being_line and
A4: c <> d ; :: thesis: ( a,b // A iff a,b // c,d )
thus ( a,b // A implies a,b // c,d ) :: thesis: ( a,b // c,d implies a,b // A )

proof

assume a,b // A ; :: thesis: a,b // c,d
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 // c,d by A1, A2, A5, A6, Th21;
hence a,b // c,d by A5, A7, Th4; :: thesis: verum

end;

assume A8: a,b // c,d ; :: thesis: a,b // A
A = Line (c,d) by A1, A2, A3, A4, Lm6;
hence a,b // A by A4, A8; :: thesis: verum