:: deftheorem defines are_COrte_wrt ANALORT:def 3 :
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V holds
( u,v,u1,v1 are_COrte_wrt x,y iff Orte (x,y,u), Orte (x,y,v) // u1,v1 );