for V being RealLinearSpace
for u, u1, v, v1, x, y being VECTOR of V
for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds
( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )