let V be RealLinearSpace; :: thesis: for u, v, u1, v1, x, y being VECTOR of V st u,v,u1,v1 are_COrte_wrt x,y holds
v,u,v1,u1 are_COrte_wrt x,y
let u, v, u1, v1, x, y be VECTOR of V; :: thesis: ( u,v,u1,v1 are_COrte_wrt x,y implies v,u,v1,u1 are_COrte_wrt x,y )
assume u,v,u1,v1 are_COrte_wrt x,y ; :: thesis: v,u,v1,u1 are_COrte_wrt x,y
then Orte (x,y,u), Orte (x,y,v) // u1,v1 by Def3;
then Orte (x,y,v), Orte (x,y,u) // v1,u1 by ANALOAF:12;
hence v,u,v1,u1 are_COrte_wrt x,y by Def3; :: thesis: verum