let n be Element of NAT ; :: thesis: for p being Point of (TOP-REAL 2)
for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
1 < I
let p be Point of (TOP-REAL 2); :: thesis: for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
1 < I
let C be compact non vertical Subset of (TOP-REAL 2); :: thesis: for I being Integer st p in BDD C & I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
1 < I
set W = W-bound C;
set E = E-bound C;
set pW = (p `1 ) - (W-bound C);
set EW = (E-bound C) - (W-bound C);
let I be Integer; :: thesis: ( p in BDD C & I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] implies 1 < I )
assume A1: ( p in BDD C & I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] ) ; :: thesis: 1 < I
then A2: W-bound C <= W-bound (BDD C) by Th18;
A3: (E-bound C) - (W-bound C) > 0 by SPRECT_1:33, XREAL_1:52;
set K = [\((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/];
BDD C is Bounded by JORDAN2C:114;
then p `1 >= W-bound (BDD C) by A1, Th6;
then p `1 >= W-bound C by A2, XXREAL_0:2;
then (p `1 ) - (W-bound C) >= 0 by XREAL_1:50;
then A4: ((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 1 >= 0 + 1 by A3, XREAL_1:8;
((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) - 1 < [\((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] by INT_1:def 4;
then (((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) - 1) + 2 < [\((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] + 2 by XREAL_1:8;
then 1 < [\((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] + 2 by A4, XXREAL_0:2;
hence 1 < I by A1, INT_1:51; :: thesis: verum