let C be Simple_closed_curve; :: thesis: for i being Element of NAT
for r, t being real number st r > 0 & t > 0 holds
ex n being Element of NAT st
( i < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )
let i be Element of NAT ; :: thesis: for r, t being real number st r > 0 & t > 0 holds
ex n being Element of NAT st
( i < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )
let r, t be real number ; :: thesis: ( r > 0 & t > 0 implies ex n being Element of NAT st
( i < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t ) )
assume
( r > 0 & t > 0 )
; :: thesis: ex n being Element of NAT st
( i < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )
then consider n being Element of NAT such that
1 < n
and
A1:
( dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )
by GOBRD14:21;
per cases
( i < n or i >= n )
;
suppose A2:
i < n
;
:: thesis: ex n being Element of NAT st
( i < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )take
n
;
:: thesis: ( i < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )thus
(
i < n &
dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 1,2) < r &
dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 2,1) < t )
by A1, A2;
:: thesis: verum end; suppose A3:
i >= n
;
:: thesis: ex n being Element of NAT st
( i < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )take
i + 1
;
:: thesis: ( i < i + 1 & dist ((Gauge C,(i + 1)) * 1,1),((Gauge C,(i + 1)) * 1,2) < r & dist ((Gauge C,(i + 1)) * 1,1),((Gauge C,(i + 1)) * 2,1) < t )thus A4:
i < i + 1
by NAT_1:13;
:: thesis: ( dist ((Gauge C,(i + 1)) * 1,1),((Gauge C,(i + 1)) * 1,2) < r & dist ((Gauge C,(i + 1)) * 1,1),((Gauge C,(i + 1)) * 2,1) < t )then A5:
dist ((Gauge C,(i + 1)) * 1,1),
((Gauge C,(i + 1)) * 2,1) < dist ((Gauge C,i) * 1,1),
((Gauge C,i) * 2,1)
by Th11;
A6:
(
i > n or
i = n )
by A3, XXREAL_0:1;
then
dist ((Gauge C,i) * 1,1),
((Gauge C,i) * 2,1) <= dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 2,1)
by Th11;
then A7:
dist ((Gauge C,(i + 1)) * 1,1),
((Gauge C,(i + 1)) * 2,1) < dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 2,1)
by A5, XXREAL_0:2;
A8:
dist ((Gauge C,(i + 1)) * 1,1),
((Gauge C,(i + 1)) * 1,2) < dist ((Gauge C,i) * 1,1),
((Gauge C,i) * 1,2)
by A4, Th9;
dist ((Gauge C,i) * 1,1),
((Gauge C,i) * 1,2) <= dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 1,2)
by A6, Th9;
then
dist ((Gauge C,(i + 1)) * 1,1),
((Gauge C,(i + 1)) * 1,2) < dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 1,2)
by A8, XXREAL_0:2;
hence
(
dist ((Gauge C,(i + 1)) * 1,1),
((Gauge C,(i + 1)) * 1,2) < r &
dist ((Gauge C,(i + 1)) * 1,1),
((Gauge C,(i + 1)) * 2,1) < t )
by A1, A7, XXREAL_0:2;
:: thesis: verum end;