set n = 2;

per cases ( |.(r - (((c_n r) . 2) / ((c_d r) . 2))).| < 1 / ((sqrt 5) * (((c_d r) . 2) |^ 2)) or |.(r - (((c_n r) . (2 + 1)) / ((c_d r) . (2 + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . (2 + 1)) |^ 2)) or |.(r - (((c_n r) . (2 + 2)) / ((c_d r) . (2 + 2)))).| < 1 / ((sqrt 5) * (((c_d r) . (2 + 2)) |^ 2)) ) by Th5;

suppose A3: |.(r - (((c_n r) . 2) / ((c_d r) . 2))).| < 1 / ((sqrt 5) * (((c_d r) . 2) |^ 2)) ; :: thesis: not HWZSet1 r is empty

set q1 = (c_n r) . 2;
reconsider q2 = (c_d r) . 2 as Element of INT by NUMBERS:17, REAL_3:50;
set q = ((c_n r) . 2) / q2;
A5: (c_n r) . 2,q2 are_coprime by Th4;
|.(r - (((c_n r) . 2) / q2)).| < 1 / ((sqrt 5) * ((denominator (((c_n r) . 2) / q2)) |^ 2)) by Th8, A3, A5;
then ((c_n r) . 2) / q2 in HWZSet r ;
then denominator (((c_n r) . 2) / q2) in HWZSet1 r ;
hence not HWZSet1 r is empty by XBOOLE_0:def 1; :: thesis: verum

end;

suppose A8: |.(r - (((c_n r) . (2 + 1)) / ((c_d r) . (2 + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . (2 + 1)) |^ 2)) ; :: thesis: not HWZSet1 r is empty

set q1 = (c_n r) . (2 + 1);
reconsider q2 = (c_d r) . (2 + 1) as Element of INT by NUMBERS:17, REAL_3:50;
set q = ((c_n r) . (2 + 1)) / q2;
(c_n r) . (2 + 1),q2 are_coprime by Th4;
then ( (c_n r) . (2 + 1) = numerator (((c_n r) . (2 + 1)) / q2) & q2 = denominator (((c_n r) . (2 + 1)) / q2) ) by Th8;
then ((c_n r) . (2 + 1)) / q2 in HWZSet r by A8;
then denominator (((c_n r) . (2 + 1)) / q2) in HWZSet1 r ;
hence not HWZSet1 r is empty by XBOOLE_0:def 1; :: thesis: verum

end;

suppose A14: |.(r - (((c_n r) . (2 + 2)) / ((c_d r) . (2 + 2)))).| < 1 / ((sqrt 5) * (((c_d r) . (2 + 2)) |^ 2)) ; :: thesis: not HWZSet1 r is empty

set q1 = (c_n r) . (2 + 2);
reconsider q2 = (c_d r) . (2 + 2) as Element of INT by NUMBERS:17, REAL_3:50;
set q = ((c_n r) . (2 + 2)) / q2;
(c_n r) . (2 + 2),q2 are_coprime by Th4;
then |.(r - (((c_n r) . (2 + 2)) / q2)).| < 1 / ((sqrt 5) * ((denominator (((c_n r) . (2 + 2)) / q2)) |^ 2)) by Th8, A14;
then ((c_n r) . (2 + 2)) / q2 in HWZSet r ;
then denominator (((c_n r) . (2 + 2)) / q2) in HWZSet1 r ;
hence not HWZSet1 r is empty by XBOOLE_0:def 1; :: thesis: verum

end;

end;