let V be RealLinearSpace; :: thesis: for x, y, u, u1, v, v1 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y holds
v,v1,u,u1 are_COrtm_wrt x,y
let x, y, u, u1, v, v1 be VECTOR of V; :: thesis: ( Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y implies v,v1,u,u1 are_COrtm_wrt x,y )
assume A1: Gen x,y ; :: thesis: ( not u,u1,v,v1 are_COrtm_wrt x,y or v,v1,u,u1 are_COrtm_wrt x,y )
assume u,u1,v,v1 are_COrtm_wrt x,y ; :: thesis: v,v1,u,u1 are_COrtm_wrt x,y
then Ortm (x,y,u), Ortm (x,y,u1) // v,v1 by Def4;
then v,v1 // Ortm (x,y,u), Ortm (x,y,u1) by ANALOAF:21;
then Ortm (x,y,v), Ortm (x,y,v1) // Ortm (x,y,(Ortm (x,y,u))), Ortm (x,y,(Ortm (x,y,u1))) by A1, Th17;
then Ortm (x,y,v), Ortm (x,y,v1) // u, Ortm (x,y,(Ortm (x,y,u1))) by A1, Th7;
then Ortm (x,y,v), Ortm (x,y,v1) // u,u1 by A1, Th7;
hence v,v1,u,u1 are_COrtm_wrt x,y by Def4; :: thesis: verum