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

now :: thesis: not (succ A) \ Z <> {}

assume (succ A) \ Z <> {} ; :: thesis: contradiction
then consider C being Ordinal such that
A3: C in (succ A) \ Z and
A4: for B being Ordinal st B in (succ A) \ Z holds
C c= B by Th16;

now :: thesis: for B being Ordinal st B in C holds
P₁[B]

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 :: thesis: B in Z

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 A4;
C <> B by A5;
then C c< B by A7;
hence contradiction by A5, Th7; :: thesis: verum

end;

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

end;

then A8: P₁[C] by A1;
not C in Z by A3, XBOOLE_0:def 5;
hence contradiction by A2, A3, A8; :: 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, Th2;
hence P₁[A] ; :: thesis: verum