let AS be AffinSpace; :: thesis: 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; :: thesis: ( 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; :: thesis: verum