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