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