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

A6: now

assume that
A7: u <> v and
A8: u1 <> v1 ; :: thesis: ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y )
u1,v1 // u1,w by A1, A4, A5, A7, Th6, ANALOAF:20;
then A9: ( u1,v1 // v1,w or u1,w // w,v1 ) by ANALOAF:23;

now

assume A10: u1 <> w ; :: thesis: ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y )
A11: u1,v1 // Ortm x,y,u, Ortm x,y,v by A4, ANALOAF:21;
u1,w // Ortm x,y,u, Ortm x,y,v by A5, ANALOAF:21;
then ( Ortm x,y,u, Ortm x,y,v // v1,w or Ortm x,y,u, Ortm x,y,v // w,v1 ) by A8, A9, A10, A11, ANALOAF:20;
hence ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y ) by Def4; :: thesis: verum

end;

hence ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y ) by A2; :: thesis: verum

end;

now

assume u = v ; :: thesis: ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y )
then ( Ortm x,y,u, Ortm x,y,v // v1,w or Ortm x,y,u, Ortm x,y,v // w,v1 ) by ANALOAF:18;
hence ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y ) by Def4; :: thesis: verum

end;

hence ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y ) by A3, A6; :: thesis: verum