let n be Nat; :: thesis: for r being Real st r is irrational holds
|.(r - (((c_n r) . n) / ((c_d r) . n))).| > 0
let r be Real; :: thesis: ( r is irrational implies |.(r - (((c_n r) . n) / ((c_d r) . n))).| > 0 )
assume A1: r is irrational ; :: thesis: |.(r - (((c_n r) . n) / ((c_d r) . n))).| > 0
assume not |.(r - (((c_n r) . n) / ((c_d r) . n))).| > 0 ; :: thesis: contradiction
then |.(r - (((c_n r) . n) / ((c_d r) . n))).| = 0 by COMPLEX1:46;
then A3: r - (((c_n r) . n) / ((c_d r) . n)) = 0 by COMPLEX1:45;
(c_d r) . n in NAT by REAL_3:50;
hence contradiction by A1, A3; :: thesis: verum