let AS be AffinSpace; for a, b, c, d being Element of AS st c in Line (a,b) & a <> b holds
( d in Line (a,b) iff a,b // c,d )
let a, b, c, d be Element of AS; ( c in Line (a,b) & a <> b implies ( d in Line (a,b) iff a,b // c,d ) )
assume that
A1:
c in Line (a,b)
and
A2:
a <> b
; ( d in Line (a,b) iff a,b // c,d )
A3:
LIN a,b,c
by A1, Def2;
thus
( d in Line (a,b) implies a,b // c,d )
( a,b // c,d implies d in Line (a,b) )
assume
a,b // c,d
; d in Line (a,b)
then
LIN a,b,d
by A2, A3, Th8;
hence
d in Line (a,b)
by Def2; verum