take omega ; :: thesis: for b₁ being natural number holds b₁ in omega
let y be natural number ; :: thesis: y in omega
thus y in omega by Def13; :: thesis: verum