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