let C be non empty compact Subset of (TOP-REAL 2); :: thesis: ( NW-corner C = SW-corner C implies C is horizontal )
assume NW-corner C = SW-corner C ; :: thesis: C is horizontal
then S-bound C = N-bound C by SPPOL_2:1;
hence C is horizontal by Th16; :: thesis: verum