let S be Simple_closed_curve; :: thesis: ( not S is vertical & not S is horizontal )
consider p1 being object such that
A1: p1 in S by XBOOLE_0:def 1;
reconsider p1 = p1 as Point of (TOP-REAL 2) by A1;
ex p2 being Point of (TOP-REAL 2) st
( p2 in S & p2 `1 <> p1 `1 ) by Th15;
hence not S is vertical by A1, SPPOL_1:def 3; :: thesis: not S is horizontal
ex p2 being Point of (TOP-REAL 2) st
( p2 in S & p2 `2 <> p1 `2 ) by Th14;
hence not S is horizontal by A1, SPPOL_1:def 2; :: thesis: verum