let V be RealLinearSpace; :: thesis: for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrte_wrt x,y
let u, v, w, x, y be VECTOR of V; :: thesis: u,u,v,w are_COrte_wrt x,y
Orte x,y,u, Orte x,y,u // v,w by ANALOAF:18;
hence u,u,v,w are_COrte_wrt x,y by Def3; :: thesis: verum