let S be OAffinSpace; :: thesis: 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; :: 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 that
A2: x,y // z,t and
A3: z,t // u,w ; :: thesis: x,y // u,w
z,t // x,y by A2, Th2;
hence x,y // u,w by A1, A3, ANALOAF:def 5; :: thesis: verum