let AS be AffinSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x )
thus z,t // x,y by A1, Lm1; :: thesis: ( z,t // y,x & t,z // x,y & t,z // y,x )
hence ( z,t // y,x & t,z // x,y ) by Lm2, Lm3; :: thesis: t,z // y,x
hence t,z // y,x by Lm3; :: thesis: verum