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: ( A <> 0 & ( for B being Ordinal holds A <> succ B ) implies P₁[A] ) by A3, A5, ORDINAL1:29;

now :: thesis: ( ex B being Ordinal st A = succ B implies P₁[A] )

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