:: deftheorem defines E-most PSCOMP_1:def 17 :
for X being Subset of (TOP-REAL 2) holds E-most X = (LSeg ((SE-corner X),(NE-corner X))) /\ X;