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