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 that
A1: p in X and
A2: 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 = lower_bound (proj1 | X) by PSCOMP_1:def 7;
hence W-bound X <= p `1 by A1, A2, Lm7; :: thesis: ( p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X )
E-bound X = upper_bound (proj1 | X) by PSCOMP_1:def 9;
hence E-bound X >= p `1 by A1, A2, Lm7; :: thesis: ( S-bound X <= p `2 & p `2 <= N-bound X )
S-bound X = lower_bound (proj2 | X) by PSCOMP_1:def 10;
hence S-bound X <= p `2 by A1, A2, Lm8; :: thesis: p `2 <= N-bound X
N-bound X = upper_bound (proj2 | X) by PSCOMP_1:def 8;
hence p `2 <= N-bound X by A1, A2, Lm8; :: thesis: verum