let V be RealLinearSpace; :: thesis: for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u,u1,u2,v2 are_COrtm_wrt x,y & not u2,v2,w,w1 are_COrtm_wrt x,y & not v = v1 holds
u = u1
let x, y, u, u1, v, v1, w, w1, u2, v2 be VECTOR of V; :: thesis: ( Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u,u1,u2,v2 are_COrtm_wrt x,y & not u2,v2,w,w1 are_COrtm_wrt x,y & not v = v1 implies u = u1 )
assume A1: Gen x,y ; :: thesis: ( not u,u1,v,v1 are_COrtm_wrt x,y or not v,v1,w,w1 are_COrtm_wrt x,y or not u,u1,u2,v2 are_COrtm_wrt x,y or u2,v2,w,w1 are_COrtm_wrt x,y or v = v1 or u = u1 )
assume A2: ( u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u,u1,u2,v2 are_COrtm_wrt x,y ) ; :: thesis: ( u2,v2,w,w1 are_COrtm_wrt x,y or v = v1 or u = u1 )
then A3: Ortm x,y,u, Ortm x,y,u1 // v,v1 by Def4;
A4: Ortm x,y,v, Ortm x,y,v1 // w,w1 by A2, Def4;
A5: Ortm x,y,u, Ortm x,y,u1 // u2,v2 by A2, Def4;

now

assume A6: ( u <> u1 & v <> v1 ) ; :: thesis: ( u2,v2,w,w1 are_COrtm_wrt x,y or v = v1 or u = u1 )
then v,v1 // u2,v2 by A1, A3, A5, Th6, ANALOAF:20;
then Ortm x,y,v, Ortm x,y,v1 // Ortm x,y,u2, Ortm x,y,v2 by A1, Th17;
then Ortm x,y,u2, Ortm x,y,v2 // w,w1 by A1, A4, A6, Th6, ANALOAF:20;
hence ( u2,v2,w,w1 are_COrtm_wrt x,y or v = v1 or u = u1 ) by Def4; :: thesis: verum

end;

hence ( u2,v2,w,w1 are_COrtm_wrt x,y or v = v1 or u = u1 ) ; :: thesis: verum