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