take omega ; :: thesis: for b₁ being Nat holds b₁ in omega
let y be Nat; :: thesis: y in omega
thus y in omega by Def12; :: thesis: verum