let S be OAffinSpace; for x, y, z, t, u, w being Element of S st z <> t & x,y // z,t & z,t // u,w holds
x,y // u,w
let x, y, z, t, u, w be Element of S; ( z <> t & x,y // z,t & z,t // u,w implies x,y // u,w )
assume A1:
z <> t
; ( not x,y // z,t or not z,t // u,w or x,y // u,w )
assume that
A2:
x,y // z,t
and
A3:
z,t // u,w
; x,y // u,w
z,t // x,y
by A2, Th2;
hence
x,y // u,w
by A1, A3, ANALOAF:def 5; verum