let a be positive non heavy Real; :: thesis: for b being positive Real holds a + b > a * b
let b be positive Real; :: thesis: a + b > a * b
( (1 / a) + (1 / b) is heavy & (1 / a) + (1 / b) is positive ) ;
hence a + b > a * b by SIL; :: thesis: verum