let S be OAffinSpace; :: thesis: Lambda S is AffinSpace
set AS = Lambda S;
A1: ( ( for x, y, z being Element of (Lambda S) ex t being Element of (Lambda S) st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of (Lambda S) ex t being Element of (Lambda S) st
( x,y // z,t & x,z // y,t ) ) ) by Th39;
A2: for x, y, z, t being Element of (Lambda S) st z,x // x,t & x <> z holds
ex u being Element of (Lambda S) st
( y,x // x,u & y,z // t,u ) by Th39;
( ( for x, y, z, t, u, w being Element of (Lambda S) 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 S) holds x,y // x,z ) by Th39;
hence Lambda S is AffinSpace by A1, A2, Def6; :: thesis: verum