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