let C be non empty compact Subset of (TOP-REAL 2); :: thesis: ( NW-corner C = NE-corner C implies C is vertical )
assume NW-corner C = NE-corner C ; :: thesis: C is vertical
then W-bound C = E-bound C by SPPOL_2:1;
hence C is vertical by Th15; :: thesis: verum