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

now

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

end;

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