defpred S₁[ Ordinal] means ( a in $1 & $1 is epsilon );
A1: ex c being Ordinal st S₁[c] by Th33;
consider c being Ordinal such that
A2: ( S₁[c] & ( for b being Ordinal st S₁[b] holds
c c= b ) ) from ORDINAL1:sch 1(A1);
reconsider c = c as epsilon Ordinal by A2;
take c ; :: thesis: ( a in c & ( for b being epsilon Ordinal st a in b holds
c c= b ) )
thus ( a in c & ( for b being epsilon Ordinal st a in b holds
c c= b ) ) by A2; :: thesis: verum