let C be non empty compact Subset of (TOP-REAL 2); :: thesis: ( C is vertical iff E-bound C <= W-bound C )
A1: E-bound C >= W-bound C by SPRECT_1:21;
( C is vertical iff W-bound C = E-bound C ) by SPRECT_1:15;
hence ( C is vertical iff E-bound C <= W-bound C ) by A1, XXREAL_0:1; :: thesis: verum