:: deftheorem Def6 defines CORTM ANALORT:def 6 :
for V being RealLinearSpace
for x, y being VECTOR of V
for b₄ being Relation of [: the carrier of V, the carrier of V:] holds
( b₄ = CORTM (V,x,y) iff for uu, vv being object holds
( [uu,vv] in b₄ iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) );