let AS be AffinSpace; :: thesis: for c, d, a, b 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 c, d, a, b 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 )
A5: ( a,b // A implies a,b // c,d )

proof

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

end;

( a,b // c,d implies a,b // A )

proof

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

end;

hence ( a,b // A iff a,b // c,d ) by A5; :: thesis: verum