let AS be AffinSpace; :: thesis: for c, a, b, d being Element of AS st c in Line a,b & d in Line a,b & c <> d holds
Line c,d c= Line a,b
let c, a, b, d be Element of AS; :: thesis: ( c in Line a,b & d in Line a,b & c <> d implies Line c,d c= Line a,b )
assume that
A1: c in Line a,b and
A2: d in Line a,b and
A3: c <> d ; :: thesis: Line c,d c= Line a,b
A4: LIN a,b,d by A2, Def2;
A5: LIN a,b,c by A1, Def2;

now

let x be set ; :: thesis: ( x in Line c,d implies x in Line a,b )
assume A6: x in Line c,d ; :: thesis: x in Line a,b
then reconsider x9 = x as Element of AS ;
LIN c,d,x9 by A6, Def2;
then LIN a,b,x9 by A3, A5, A4, Th20;
hence x in Line a,b by Def2; :: thesis: verum

end;

hence Line c,d c= Line a,b by TARSKI:def 3; :: thesis: verum