let C be Simple_closed_curve; :: thesis: for n being Nat
for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1
let n be Nat; :: thesis: for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1
let p be Point of (TOP-REAL 2); :: thesis: for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1
set W = W-bound C;
set EW = (E-bound C) - (W-bound C);
set PW = (p `1) - (W-bound C);
set KI = [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/];
let I be Integer; :: thesis: ( I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] implies (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1 )
A1: (E-bound C) - (W-bound C) > 0 by TOPREAL5:17, XREAL_1:50;
2 |^ n > 0 by NEWTON:83;
then A2: (((E-bound C) - (W-bound C)) / (2 |^ n)) * ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) = (p `1) - (W-bound C) by A1, Lm2;
assume I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] ; :: thesis: (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1
then A3: I - 2 = [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] by Lm1;
[\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] <= (((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n) by INT_1:def 6;
then A4: (((E-bound C) - (W-bound C)) / (2 |^ n)) * [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] <= (((E-bound C) - (W-bound C)) / (2 |^ n)) * ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) by A1, XREAL_1:64;
(W-bound C) + ((p `1) - (W-bound C)) = p `1 ;
hence (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1 by A3, A2, A4, XREAL_1:6; :: thesis: verum