for AS being AffinSpace
for x, y, z being Element of AS holds
( x,y // z,z & z,z // x,y ) by Lm1, DIRAF:40;