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