consider A being Ordinal such that
A2: P₁[A] by A1;
defpred S₁[ object ] means ex B being Ordinal st
( $1 = B & P₁[B] );
consider X being set such that
A3: for x being object holds
( x in X iff ( x in succ A & S₁[x] ) ) from XBOOLE_0:sch 1();
for a being object st a in X holds
a in succ A by A3;
then A4: X c= succ A ;
A in succ A by Th2;
then X <> {} by A2, A3;
then consider C being Ordinal such that
A5: C in X and
A6: for B being Ordinal st B in X holds
C c= B by A4, Th16;
C in succ A by A3, A5;
then A7: C c= succ A by Def2;
take C ; :: thesis: ( P₁[C] & ( for B being Ordinal st P₁[B] holds
C c= B ) )
ex B being Ordinal st
( C = B & P₁[B] ) by A3, A5;
hence P₁[C] ; :: thesis: for B being Ordinal st P₁[B] holds
C c= B
let B be Ordinal; :: thesis: ( P₁[B] implies C c= B )
assume A8: P₁[B] ; :: thesis: C c= B
assume A9: not C c= B ; :: thesis: contradiction
then B c< C ;
then B in C by Th7;
then B in X by A3, A8, A7;
hence contradiction by A6, A9; :: thesis: verum