A4: for A being Ordinal st ( for B being Ordinal st B in A holds
P₁[B] ) holds
P₁[A]

proof

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
P₁[B] ) implies P₁[A] )
assume A5: for B being Ordinal st B in A holds
P₁[B] ; :: thesis: P₁[A]

A6: now

given B being Ordinal such that A7: A = succ B ; :: thesis: P₁[A]
B in A by A7, ORDINAL1:10;
hence P₁[A] by A2, A5, A7; :: thesis: verum

end;

now

assume A8: ( A <> {} & ( for B being Ordinal holds A <> succ B ) ) ; :: thesis: P₁[A]
then A is limit_ordinal by ORDINAL1:42;
hence P₁[A] by A3, A5, A8; :: thesis: verum

end;

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

end;

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