let P be Subset of (TOP-REAL 2); :: thesis: ( not P is trivial & P is horizontal implies not P is vertical )
assume that
A1: not P is trivial and
A2: ( ( for p, q being Point of (TOP-REAL 2) st p in P & q in P holds
p `2 = q `2 ) & ( for p, q being Point of (TOP-REAL 2) st p in P & q in P holds
p `1 = q `1 ) ) ; :: according to SPPOL_1:def 2,SPPOL_1:def 3 :: thesis: contradiction
consider p, q being Point of (TOP-REAL 2) such that
A3: ( p in P & q in P ) and
A4: p <> q by A1, SUBSET_1:45;
( p `2 = q `2 & p `1 = q `1 ) by A2, A3;
hence contradiction by A4, TOPREAL3:6; :: thesis: verum