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