let A be Ordinal; :: thesis: P₁[A]
set Y = succ A;
defpred S₁[ set ] means ex B being Ordinal st
( $1 = B & P₁[B] );
consider Z being set such that
A2: for x being set holds
( x in Z iff ( x in succ A & S₁[x] ) ) from XBOOLE_0:sch 1();

now

assume (succ A) \ Z <> {} ; :: thesis: contradiction
then consider C being Ordinal such that
A3: ( C in (succ A) \ Z & ( for B being Ordinal st B in (succ A) \ Z holds
C c= B ) ) by Th32;
A4: ( C in succ A & not C in Z ) by A3, XBOOLE_0:def 5;

now

let B be Ordinal; :: thesis: ( B in C implies P₁[B] )
assume A5: B in C ; :: thesis: P₁[B]
A6: C c= succ A by A3, Def2;

now

assume not B in Z ; :: thesis: contradiction
then B in (succ A) \ Z by A5, A6, XBOOLE_0:def 5;
then A7: C c= B by A3;
C <> B by A5;
then C c< B by A7, XBOOLE_0:def 8;
hence contradiction by A5, Th21; :: thesis: verum

end;

then ex B' being Ordinal st
( B = B' & P₁[B'] ) by A2;
hence P₁[B] ; :: thesis: verum

end;

then P₁[C] by A1;
hence contradiction by A2, A4; :: thesis: verum

end;

then ( not A in succ A or A in Z ) by XBOOLE_0:def 5;
then ex B being Ordinal st
( A = B & P₁[B] ) by A2, Th10;
hence P₁[A] ; :: thesis: verum