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