let n be Nat; :: thesis: for b being Element of BOOLEAN holds n * b <= n
let b be Element of BOOLEAN ; :: thesis: n * b <= n
( b = 0 or b = 1 ) by TARSKI:def 2;
hence n * b <= n ; :: thesis: verum