let UN be Universe; :: thesis: for u being Element of UN holds succ u is Element of UN
let u be Element of UN; :: thesis: succ u is Element of UN
succ u = u \/ {u} ;
hence succ u is Element of UN ; :: thesis: verum