let C be non empty compact Subset of (TOP-REAL 2); :: thesis: ( C is horizontal iff N-bound C <= S-bound C )
A1: N-bound C >= S-bound C by SPRECT_1:22;
( C is horizontal iff N-bound C = S-bound C ) by SPRECT_1:16;
hence ( C is horizontal iff N-bound C <= S-bound C ) by A1, XXREAL_0:1; :: thesis: verum