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_COrte_wrt x,y & u,v,v1,w are_COrte_wrt x,y holds
u,v,u1,w are_COrte_wrt x,y
let x, y, u, v, u1, v1, w be VECTOR of V; :: thesis: ( Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,w are_COrte_wrt x,y implies u,v,u1,w are_COrte_wrt x,y )
assume A1: Gen x,y ; :: thesis: ( not u,v,u1,v1 are_COrte_wrt x,y or not u,v,v1,w are_COrte_wrt x,y or u,v,u1,w are_COrte_wrt x,y )
assume that
A2: u,v,u1,v1 are_COrte_wrt x,y and
A3: u,v,v1,w are_COrte_wrt x,y ; :: thesis: u,v,u1,w are_COrte_wrt x,y
A4: Orte x,y,u, Orte x,y,v // u1,v1 by A2, Def3;
A5: Orte x,y,u, Orte x,y,v // v1,w by A3, Def3;
A6: u1,v1 // Orte x,y,u, Orte x,y,v by A4, ANALOAF:21;

A7: now

assume u <> v ; :: thesis: u,v,u1,w are_COrte_wrt x,y
then u1,v1 // v1,w by A1, A4, A5, Th13, ANALOAF:20;
then A8: u1,v1 // u1,w by ANALOAF:22;

now

assume u1 <> v1 ; :: thesis: u,v,u1,w are_COrte_wrt x,y
then Orte x,y,u, Orte x,y,v // u1,w by A6, A8, ANALOAF:20;
hence u,v,u1,w are_COrte_wrt x,y by Def3; :: thesis: verum

end;

hence u,v,u1,w are_COrte_wrt x,y by A3; :: thesis: verum

end;

now

assume u = v ; :: thesis: u,v,u1,w are_COrte_wrt x,y
then Orte x,y,u, Orte x,y,v // u1,w by ANALOAF:18;
hence u,v,u1,w are_COrte_wrt x,y by Def3; :: thesis: verum

end;

hence u,v,u1,w are_COrte_wrt x,y by A7; :: thesis: verum