let S be OAffinSpace; :: thesis: for x, y, z, t being Element of S st x,y // z,t holds
z,t // x,y
let x, y, z, t be Element of S; :: thesis: ( x,y // z,t implies z,t // x,y )
assume A1: x,y // z,t ; :: thesis: z,t // x,y

now

assume A2: x <> y ; :: thesis: z,t // x,y
( x,y // x,y & x,y // z,t ) by A1, Th4;
hence z,t // x,y by A2, ANALOAF:def 5; :: thesis: verum

end;

hence z,t // x,y by ANALOAF:def 5; :: thesis: verum