set S = the OAffinSpace;
A1: ( ( for x, y, z being Element of (Lambda the OAffinSpace) ex t being Element of (Lambda the OAffinSpace) st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of (Lambda the OAffinSpace) ex t being Element of (Lambda the OAffinSpace) st
( x,y // z,t & x,z // y,t ) ) ) by Th39;
A2: for x, y, z, t being Element of (Lambda the OAffinSpace) st z,x // x,t & x <> z holds
ex u being Element of (Lambda the OAffinSpace) st
( y,x // x,u & y,z // t,u ) by Th39;
( ( for x, y, z, t, u, w being Element of (Lambda the OAffinSpace) 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 (Lambda the OAffinSpace) holds x,y // x,z ) by Th39;
then ( not Lambda the OAffinSpace is trivial & Lambda the OAffinSpace is AffinSpace-like ) by A1, A2;
hence ex b₁ being non trivial AffinStruct st
( b₁ is strict & b₁ is AffinSpace-like ) ; :: thesis: verum