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 that
A1: r > 0 and
A2: 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 )
consider n being Element of NAT such that
1 < n and
A3: dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r and
A4: dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t by A1, A2, GOBRD14:21;

per cases ( i < n or i >= n ) ;

suppose A5: 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 A3, A4, A5; :: thesis: verum

end;

suppose A6: 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 )
A7: ( i > n or i = n ) by A6, XXREAL_0:1;
then A8: dist ((Gauge C,i) * 1,1),((Gauge C,i) * 2,1) <= dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) by Th11;
A9: dist ((Gauge C,i) * 1,1),((Gauge C,i) * 1,2) <= dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) by A7, Th9;
thus A10: 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 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 Th9;
then A11: 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 A9, XXREAL_0:2;
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 A10, Th11;
then 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 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 A3, A4, A11, XXREAL_0:2; :: thesis: verum

end;

end;