let n be Nat; :: thesis: for r being Real st r is irrational holds
((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)) > 0
let r be Real; :: thesis: ( r is irrational implies ((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)) > 0 )
assume A1: r is irrational ; :: thesis: ((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)) > 0
then A2: (c_d r) . (n + 1) >= 1 by Th8;
(((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n) > 0 by A1, Th12;
hence ((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)) > 0 by A2; :: thesis: verum