reconsider r = (@ f2) / (@ f1) as positive Real ;
take r ; :: thesis: ex r1, r2 being positive Real st
( r1 = f1 & r2 = f2 & r = r2 / r1 )
thus ex r1, r2 being positive Real st
( r1 = f1 & r2 = f2 & r = r2 / r1 ) ; :: thesis: verum