let V be RealLinearSpace; :: thesis: for u, u1, u2, v, v1, v2, w, w1, x, y 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 u, u1, u2, v, v1, v2, w, w1, x, y 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 that
A2: u,u1,v,v1 are_COrtm_wrt x,y and
A3: v,v1,w,w1 are_COrtm_wrt x,y and
A4: 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 )
A5: Ortm (x,y,u), Ortm (x,y,u1) // v,v1 by A2;
A6: Ortm (x,y,v), Ortm (x,y,v1) // w,w1 by A3;
A7: Ortm (x,y,u), Ortm (x,y,u1) // u2,v2 by A4;

now :: thesis: ( u <> u1 & v <> v1 & not u2,v2,w,w1 are_COrtm_wrt x,y & not v = v1 implies u = u1 )

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

end;

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