A4: for A being Ordinal st ( for B being Ordinal st B in A holds
P1[B] ) holds
P1[A]
proof
let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
P1[B] ) implies P1[A] )
assume A5: for B being Ordinal st B in A holds
P1[B] ; :: thesis: P1[A]
A6: ( A <> 0 & ( for B being Ordinal holds A <> succ B ) implies P1[A] ) by A3, A5, ORDINAL1:29;
now :: thesis: ( ex B being Ordinal st A = succ B implies P1[A] )
given B being Ordinal such that A7: A = succ B ; :: thesis: P1[A]
B in A by A7, ORDINAL1:6;
hence P1[A] by A2, A5, A7; :: thesis: verum
end;
hence P1[A] by A1, A6; :: thesis: verum
end;
thus for A being Ordinal holds P1[A] from ORDINAL1:sch 2(A4); :: thesis: verum