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