:: deftheorem defines NE-corner PSCOMP_1:def 13 :
for X being Subset of (TOP-REAL 2) holds NE-corner X = |[(E-bound X),(N-bound X)]|;