let p be Point of (TOP-REAL 2); :: thesis: for X being Subset of (TOP-REAL 2) st p in X & X is Bounded holds
( W-bound X <= p `1 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X )
let X be Subset of (TOP-REAL 2); :: thesis: ( p in X & X is Bounded implies ( W-bound X <= p `1 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X ) )
assume A1: ( p in X & X is Bounded ) ; :: thesis: ( W-bound X <= p `1 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X )
W-bound X = inf (proj1 | X) by PSCOMP_1:def 30;
hence W-bound X <= p `1 by A1, Lm7; :: thesis: ( p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X )
E-bound X = sup (proj1 | X) by PSCOMP_1:def 32;
hence E-bound X >= p `1 by A1, Lm7; :: thesis: ( S-bound X <= p `2 & p `2 <= N-bound X )
S-bound X = inf (proj2 | X) by PSCOMP_1:def 33;
hence S-bound X <= p `2 by A1, Lm8; :: thesis: p `2 <= N-bound X
N-bound X = sup (proj2 | X) by PSCOMP_1:def 31;
hence p `2 <= N-bound X by A1, Lm8; :: thesis: verum