let S be OAffinSpace; :: thesis: for x, y, z being Element of S holds
( x,y // x,z iff ( x,y // y,z or x,z // z,y ) )
let x, y, z be Element of S; :: thesis: ( x,y // x,z iff ( x,y // y,z or x,z // z,y ) )

now

assume ( x,y // y,z or x,z // z,y ) ; :: thesis: x,y // x,z
then ( x,y // x,z or x,z // x,y ) by ANALOAF:def 5;
hence x,y // x,z by Th5; :: thesis: verum

end;

hence ( x,y // x,z iff ( x,y // y,z or x,z // z,y ) ) by ANALOAF:def 5; :: thesis: verum