succ u = u \/ {u} ;
hence succ u is Element of UN ; :: thesis: verum