let AS be AffinSpace; :: thesis: for x, y, z being Element of AS holds
( x,y // z,z & z,z // x,y )
let x, y, z be Element of AS; :: thesis: ( x,y // z,z & z,z // x,y )
thus x,y // z,z by DIRAF:40; :: thesis: z,z // x,y
hence z,z // x,y by Lm1; :: thesis: verum