ex a being ordinal number st
( 0 in a & a is epsilon ) by Th33;
hence ex b₁ being ordinal number st b₁ is epsilon ; :: thesis: verum