let S be OAffinSpace; :: thesis:
let AS be non empty AffinStruct ; :: thesis:
assume A1: AS = Lambda S ; :: thesis:
hence ex x, y being Element of AS st x <> y by STRUCT_0:def 10; :: thesis:
thus 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 ) ) :: thesis:

let x, y, z, t, u, w be Element of AS; :: thesis:
reconsider x9 = x, y9 = y, z9 = z, t9 = t, u9 = u, w9 = w as Element of S by A1;
( x9,y9 '||' y9,x9 & x9,y9 '||' z9,z9 ) by Th19, Th20;
hence ( x,y // y,x & x,y // z,z ) by A1, Th38; :: thesis:
( x9 <> y9 & x9,y9 '||' z9,t9 & x9,y9 '||' u9,w9 implies z9,t9 '||' u9,w9 ) by Lm2;
hence ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) by A1, Th38; :: thesis:
( x9,y9 '||' x9,z9 implies y9,x9 '||' y9,z9 ) by Th21;
hence ( x,y // x,z implies y,x // y,z ) by A1, Th38; :: thesis:

end;

consider x9, y9, z9 being Element of S such that
A2: not x9,y9 '||' x9,z9 by Th24;
reconsider x = x9, y = y9, z = z9 as Element of AS by A1;
not x,y // x,z by A1, A2, Th38;
hence not for x, y, z being Element of AS holds x,y // x,z ; :: thesis:

end;

thus for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) :: thesis:

let x, y, z be Element of AS; :: thesis:
reconsider x9 = x, y9 = y, z9 = z as Element of S by A1;
consider t9 being Element of S such that
A3: x9,z9 '||' y9,t9 and
A4: y9 <> t9 by Th25;
reconsider t = t9 as Element of AS by A1;
x,z // y,t by A1, A3, Th38;
hence ex t being Element of AS st
( x,z // y,t & y <> t ) by A4; :: thesis:

end;

thus for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) :: thesis:

let x, y, z be Element of AS; :: thesis:
reconsider x9 = x, y9 = y, z9 = z as Element of S by A1;
consider t9 being Element of S such that
A5: ( x9,y9 '||' z9,t9 & x9,z9 '||' y9,t9 ) by Th26;
reconsider t = t9 as Element of AS by A1;
( x,y // z,t & x,z // y,t ) by A1, A5, Th38;
hence ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ; :: thesis:

end;

thus 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 ) :: thesis:

let x, y, z, t be Element of AS; :: thesis:
assume that
A6: z,x // x,t and
A7: x <> z ; :: thesis:
reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of S by A1;
z9,x9 '||' x9,t9 by A1, A6, Th38;
then consider u9 being Element of S such that
A8: ( y9,x9 '||' x9,u9 & y9,z9 '||' t9,u9 ) by A7, Th27;
reconsider u = u9 as Element of AS by A1;
( y,x // x,u & y,z // t,u ) by A1, A8, Th38;
hence ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ; :: thesis:

end;