not succ (1-element_of U) is trivial by NAT_2:def 1;
hence ex b₁ being Ordinal of U st
( not b₁ is trivial & b₁ is finite ) ; :: thesis: verum