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