let AS be AffinSpace; for a, b, c, d being Element of AS st c in Line (a,b) & d in Line (a,b) & a <> b holds
Line (a,b) c= Line (c,d)
let a, b, c, d be Element of AS; ( c in Line (a,b) & d in Line (a,b) & a <> b implies Line (a,b) c= Line (c,d) )
assume that
A1:
c in Line (a,b)
and
A2:
d in Line (a,b)
and
A3:
a <> b
; Line (a,b) c= Line (c,d)
A4:
LIN a,b,d
by A2, Def2;
A5:
LIN a,b,c
by A1, Def2;
let x be object ; TARSKI:def 3 ( not x in Line (a,b) or x in Line (c,d) )
assume A6:
x in Line (a,b)
; x in Line (c,d)
then reconsider x9 = x as Element of AS ;
LIN a,b,x9
by A6, Def2;
then
LIN c,d,x9
by A3, A5, A4, Th7;
hence
x in Line (c,d)
by Def2; verum