let S be Subset of RAT; :: thesis:
let r be Real; :: thesis:
assume that
A1: r is irrational and
A2: S = { p where p is Element of RAT : |.(r - p).| < 1 / ((denominator p) |^ 2) } ; :: thesis:
deffunc H₁( Nat) -> Element of REAL = ((c_n r) . ($1 + 1)) / ((c_d r) . ($1 + 1));
consider f being Real_Sequence such that
A3: for n being Nat holds f . n = H₁(n) from SEQ_1:sch 1();
for o being Real st o in rng f holds
o in S

let o be Real; :: thesis:
assume o in rng f ; :: thesis:
then consider i being object such that
A6: i in dom f and
A7: o = f . i by FUNCT_1:def 3;
reconsider i = i as Nat by A6;
A8: o = H₁(i) by A7, A3
.= ((c_n r) . (i + 1)) / ((c_d r) . (i + 1)) ;
A9: (c_d r) . (i + 1) in NAT by REAL_3:50;
A11: o in RAT by A8, A9, RAT_1:def 1;
reconsider o = o as Rational by A8, A9;
set cn = (c_n r) . (i + 1);
set cd = (c_d r) . (i + 1);
reconsider cd = (c_d r) . (i + 1) as Integer by A9;
( o = ((c_n r) . (i + 1)) / cd & cd <> 0 ) by A1, Th8, A8;
then consider m0 being Integer such that
(c_n r) . (i + 1) = (numerator o) * m0 and
A14: cd = (denominator o) * m0 by RAT_1:28;
A19: cd |^ 2 = cd * cd by WSIERP_1:1
.= cd * ((denominator o) * m0) by A14
.= (((denominator o) * (denominator o)) * m0) * m0 by A14
.= (((denominator o) |^ 2) * m0) * m0 by WSIERP_1:1
.= ((denominator o) |^ 2) * (m0 * m0)
.= ((denominator o) |^ 2) * (m0 |^ 2) by WSIERP_1:1 ;
A20: m0 <> 0 by A14, A1, Th8;
m0 * m0 = m0 ^2 by SQUARE_1:def 1;
then A22: m0 ^2 >= 0 + 1 by A20, SQUARE_1:12, INT_1:7;
A23: m0 |^ 2 = m0 * m0 by WSIERP_1:1
.= m0 ^2 by SQUARE_1:def 1 ;
(denominator o) |^ 2 <= ((denominator o) |^ 2) * (m0 ^2) by A22, XREAL_1:151;
then 1 / ((denominator o) |^ 2) >= 1 / (((denominator o) |^ 2) * (m0 ^2)) by XREAL_1:85;
then |.(r - o).| < 1 / ((denominator o) |^ 2) by A1, A8, A19, Th24, A23, XXREAL_0:2;
hence o in S by A2, A11; :: thesis:

end;

for n1, n2 being object st n1 in dom f & n2 in dom f & f . n1 = f . n2 holds
n1 = n2

let n1, n2 be object ; :: thesis:
assume that
A31: n1 in dom f and
A32: n2 in dom f and
A33: f . n1 = f . n2 ; :: thesis:
consider m1 being Nat such that
A34: n1 = m1 by A31;
consider m2 being Nat such that
A35: n2 = m2 by A32;
A36: f . m1 = f . n1 by A34
.= f . m2 by A33, A35 ;
A37: ((c_n r) . (m1 + 1)) / ((c_d r) . (m1 + 1)) = f . m1 by A3
.= H₁(m2) by A36, A3
.= ((c_n r) . (m2 + 1)) / ((c_d r) . (m2 + 1)) ;
assume n1 <> n2 ; :: thesis:

then m1 + 1 > m2 + 1 by XREAL_1:8;
then |.(r - (((c_n r) . (m1 + 1)) / ((c_d r) . (m1 + 1)))).| < |.(r - (((c_n r) . (m2 + 1)) / ((c_d r) . (m2 + 1)))).| by A1, Th23;
hence contradiction by A37; :: thesis:

end;

then m1 + 1 < m2 + 1 by XREAL_1:8;
then |.(r - (((c_n r) . (m1 + 1)) / ((c_d r) . (m1 + 1)))).| > |.(r - (((c_n r) . (m2 + 1)) / ((c_d r) . (m2 + 1)))).| by A1, Th23;
hence contradiction by A37; :: thesis:

end;

end;