theorem :: ANALORT:29

for V being RealLinearSpace
for u, u1, v, v1, x, y being VECTOR of V st Gen x,y holds
( u,v,u1,v1 are_Ort_wrt x,y iff ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) )