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