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

assume that
A7: A <> {} and
A8: for B being Ordinal holds A <> succ B ; :: thesis: P₁[A]
A is limit_ordinal by A8, ORDINAL1:29;
hence P₁[A] by A3, A5, A7; :: thesis: verum

end;

now

given B being Ordinal such that A9: A = succ B ; :: thesis: P₁[A]
B in A by A9, ORDINAL1:6;
hence P₁[A] by A2, A5, A9; :: 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