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 that
A2: u,v,u1,v1 are_COrtm_wrt x,y and
A3: u,v,v1,u1 are_COrtm_wrt x,y ; :: thesis: ( u = v or u1 = v1 )
assume that
A4: u <> v and
A5: u1 <> v1 ; :: thesis: contradiction
A6: Ortm (x,y,u), Ortm (x,y,v) // u1,v1 by A2, Def4;
A7: Ortm (x,y,u), Ortm (x,y,v) // v1,u1 by A3, Def4;
Ortm (x,y,u) <> Ortm (x,y,v) by A1, A4, Th6;
hence contradiction by A5, A6, A7, ANALOAF:10, ANALOAF:11; :: thesis: verum