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 :: thesis: ( ( x,y // y,z or x,z // z,y ) implies x,y // x,z )

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 Th2; :: thesis: verum

end;

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