let S be OAffinSpace; 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; ( x,y // x,z iff ( x,y // y,z or x,z // z,y ) )
now ( ( x,y // y,z or x,z // z,y ) implies x,y // x,z )assume
(
x,
y // y,
z or
x,
z // z,
y )
;
x,y // x,zthen
(
x,
y // x,
z or
x,
z // x,
y )
by ANALOAF:def 5;
hence
x,
y // x,
z
by Th2;
verum end;
hence
( x,y // x,z iff ( x,y // y,z or x,z // z,y ) )
by ANALOAF:def 5; verum