let Y, X, Z be set ; :: thesis: for A being Ordinal st A <> {} & A is limit_ordinal & Y in Tarski-Class X,A & ( Z c= Y or Z = bool Y ) holds
Z in Tarski-Class X,A
let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & Y in Tarski-Class X,A & ( Z c= Y or Z = bool Y ) implies Z in Tarski-Class X,A )
assume A1: ( A <> {} & A is limit_ordinal & Y in Tarski-Class X,A ) ; :: thesis: ( ( not Z c= Y & not Z = bool Y ) or Z in Tarski-Class X,A )
then consider B being Ordinal such that
A2: ( B in A & Y in Tarski-Class X,B ) by Th16;
A3: bool Y in Tarski-Class X,(succ B) by A2, Th13;
A4: ( Z c= Y implies Z in Tarski-Class X,(succ B) ) by A2, Th13;
A5: succ B in A by A1, A2, ORDINAL1:41;
assume ( Z c= Y or Z = bool Y ) ; :: thesis: Z in Tarski-Class X,A
hence Z in Tarski-Class X,A by A1, A3, A4, A5, Th16; :: thesis: verum