let AS be AffinSpace; for a, b being Element of AS holds
( a in Line (a,b) & b in Line (a,b) )
let a, b be Element of AS; ( a in Line (a,b) & b in Line (a,b) )
A1:
LIN a,b,b
by Th6;
LIN a,b,a
by Th6;
hence
( a in Line (a,b) & b in Line (a,b) )
by A1, Def2; verum