let P be Subset of (TOP-REAL 2); :: thesis: ( not P is vertical implies not P is empty )
assume not P is vertical ; :: thesis: not P is empty
then ex p, q being Point of (TOP-REAL 2) st
( p in P & q in P & p `1 <> q `1 ) by SPPOL_1:def 3;
hence not P is empty ; :: thesis: verum