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 & d in A ) and
A2: A is being_line and
A3: c <> d ; :: thesis: ( a,b // A iff a,b // c,d )
A4: ( 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
A5: ( p <> q & A = Line p,q & a,b // p,q ) by Def4;
p,q // c,d by A1, A5, Th36;
hence a,b // c,d by A5, Th14; :: thesis: verum

end;

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

proof

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

end;

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