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 & u2,v2,w,w1 are_COrtm_wrt x,y & not u,u1,u2,v2 are_COrtm_wrt x,y & not v = v1 holds
w = w1
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 & u2,v2,w,w1 are_COrtm_wrt x,y & not u,u1,u2,v2 are_COrtm_wrt x,y & not v = v1 implies w = w1 )
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 u2,v2,w,w1 are_COrtm_wrt x,y or u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 )
assume that
A2: u,u1,v,v1 are_COrtm_wrt x,y and
A3: v,v1,w,w1 are_COrtm_wrt x,y and
A4: u2,v2,w,w1 are_COrtm_wrt x,y ; :: thesis: ( u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 )
Ortm (x,y,u), Ortm (x,y,u1) // v,v1 by A2, Def4;
then A5: v,v1 // Ortm (x,y,u), Ortm (x,y,u1) by ANALOAF:12;
w,w1,v,v1 are_COrtm_wrt x,y by A1, A3, Th19;
then Ortm (x,y,w), Ortm (x,y,w1) // v,v1 by Def4;
then A6: v,v1 // Ortm (x,y,w), Ortm (x,y,w1) by ANALOAF:12;
w,w1,u2,v2 are_COrtm_wrt x,y by A1, A4, Th19;
then A7: Ortm (x,y,w), Ortm (x,y,w1) // u2,v2 by Def4;

now

assume that
A8: w <> w1 and
A9: v <> v1 ; :: thesis: ( u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 )
Ortm (x,y,w), Ortm (x,y,w1) // Ortm (x,y,u), Ortm (x,y,u1) by A5, A6, A9, ANALOAF:11;
then Ortm (x,y,u), Ortm (x,y,u1) // u2,v2 by A1, A7, A8, Th6, ANALOAF:11;
hence ( u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 ) by Def4; :: thesis: verum

end;

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