let V be RealLinearSpace; :: thesis: for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y & not u = v holds
u1 = v1
let x, y, u, v, u1, v1 be VECTOR of V; :: thesis: ( Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y & not u = v implies u1 = v1 )
assume A1: Gen x,y ; :: thesis: ( not u,v,u1,v1 are_COrtm_wrt x,y or not u,v,v1,u1 are_COrtm_wrt x,y or u = v or u1 = v1 )
assume A2: ( u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y ) ; :: thesis: ( u = v or u1 = v1 )
assume A3: ( u <> v & u1 <> v1 ) ; :: thesis: contradiction
A4: ( Ortm x,y,u, Ortm x,y,v // u1,v1 & Ortm x,y,u, Ortm x,y,v // v1,u1 ) by A2, Def4;
Ortm x,y,u <> Ortm x,y,v by A1, A3, Th6;
hence contradiction by A3, A4, ANALOAF:19, ANALOAF:20; :: thesis: verum