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