let V be RealLinearSpace; :: thesis: for u, v, x, y being VECTOR of V holds u,v, Ortm x,y,u, Ortm x,y,v are_COrtm_wrt x,y
let u, v, x, y be VECTOR of V; :: thesis: u,v, Ortm x,y,u, Ortm x,y,v are_COrtm_wrt x,y
Ortm x,y,u, Ortm x,y,v // Ortm x,y,u, Ortm x,y,v by ANALOAF:17;
hence u,v, Ortm x,y,u, Ortm x,y,v are_COrtm_wrt x,y by Def4; :: thesis: verum