let C be Simple_closed_curve; :: thesis: for i being Nat
for r, t being Real st r > 0 & t > 0 holds
ex n being 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 Nat; :: thesis: for r, t being Real st r > 0 & t > 0 holds
ex n being 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; :: thesis: ( r > 0 & t > 0 implies ex n being 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 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 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:11;
per cases ( i < n or i >= n ) ;
suppose A5: i < n ; :: thesis: ex n being 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 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;