let M be Cardinal; :: thesis: P₁[M]
defpred S₁[ Ordinal] means ( $1 is Cardinal implies P₁[$1] );
A4: for A being Ordinal st ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A5: for B being Ordinal st B in A holds
S₁[B] and
A6: A is Cardinal ; :: thesis: P₁[A]
reconsider M = A as Cardinal by A6;

A7: now :: thesis: ( not M is limit_cardinal implies P₁[M] )

assume not M is limit_cardinal ; :: thesis: P₁[M]
then consider N being Cardinal such that
A8: M = nextcard N ;
N in M by A8, Th17;
hence P₁[M] by A2, A5, A8; :: thesis: verum

end;

now :: thesis: ( M <> {} & M is limit_cardinal implies P₁[M] )

assume A9: ( M <> {} & M is limit_cardinal ) ; :: thesis: P₁[M]
for N being Cardinal st N in M holds
P₁[N] by A5;
hence P₁[M] by A3, A9; :: thesis: verum

end;

hence P₁[A] by A1, A7; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A4);
hence P₁[M] ; :: thesis: verum