let AS be AffinSpace; for x, y, z, t being Element of AS st x,y // z,t holds
( x,y // t,z & y,x // z,t & y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x )
let x, y, z, t be Element of AS; ( x,y // z,t implies ( x,y // t,z & y,x // z,t & y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x ) )
assume A1:
x,y // z,t
; ( x,y // t,z & y,x // z,t & y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x )
hence
( x,y // t,z & y,x // z,t )
by Lm2, Lm3; ( y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x )
hence
y,x // t,z
by Lm2; ( z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x )
thus
z,t // x,y
by A1, Lm1; ( z,t // y,x & t,z // x,y & t,z // y,x )
hence
( z,t // y,x & t,z // x,y )
by Lm2, Lm3; t,z // y,x
hence
t,z // y,x
by Lm3; verum