let S be OAffinSpace; :: thesis: for x, y, z, t being Element of S st x,y // z,t holds
( y,x // t,z & z,t // x,y & t,z // y,x )
let x, y, z, t be Element of S; :: thesis: ( x,y // z,t implies ( y,x // t,z & z,t // x,y & t,z // y,x ) )
assume x,y // z,t ; :: thesis: ( y,x // t,z & z,t // x,y & t,z // y,x )
hence ( y,x // t,z & z,t // x,y ) by Lm1, ANALOAF:def 5; :: thesis: t,z // y,x
hence t,z // y,x by ANALOAF:def 5; :: thesis: verum