:: deftheorem Def5 defines CORTE ANALORT:def 5 :
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₄ = CORTE (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_COrte_wrt x,y ) ) );