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 and
A3: 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
A4: ( p in P & q in P ) and
A5: p <> q by A1, REALSET1:15;
( p `2 = q `2 & p `1 = q `1 ) by A2, A3, A4;
hence contradiction by A5, TOPREAL3:11; :: thesis: verum