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