for AS being AffinSpace holds
( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) ) by Def6, STRUCT_0:def 10;