let i, m be Nat; :: thesis: for D being non empty Subset of (TOP-REAL 2) st m + 1 < len (Gauge (D,i)) holds
(2 * m) -' 1 < len (Gauge (D,(i + 1)))
let D be non empty Subset of (TOP-REAL 2); :: thesis: ( m + 1 < len (Gauge (D,i)) implies (2 * m) -' 1 < len (Gauge (D,(i + 1))) )
assume m + 1 < len (Gauge (D,i)) ; :: thesis: (2 * m) -' 1 < len (Gauge (D,(i + 1)))
then m + 1 < (2 |^ i) + 3 by JORDAN8:def 1;
then (2 * (m + 1)) -' 2 < (2 |^ (i + 1)) + 3 by Lm13;
then ((2 * m) + (2 * 1)) -' 2 < (2 |^ (i + 1)) + 3 ;
then A1: 2 * m < (2 |^ (i + 1)) + 3 by NAT_D:34;
(2 * m) -' 1 <= 2 * m by NAT_D:44;
then (2 * m) -' 1 < (2 |^ (i + 1)) + 3 by A1, XXREAL_0:2;
hence (2 * m) -' 1 < len (Gauge (D,(i + 1))) by JORDAN8:def 1; :: thesis: verum