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