let Y, X, Z be set ; 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; ( 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 that
A1:
A <> {}
and
A2:
A is limit_ordinal
and
A3:
Y in Tarski-Class X,A
; ( ( not Z c= Y & not Z = bool Y ) or Z in Tarski-Class X,A )
consider B being Ordinal such that
A4:
B in A
and
A5:
Y in Tarski-Class X,B
by A1, A2, A3, Th16;
A6:
bool Y in Tarski-Class X,(succ B)
by A5, Th13;
A7:
( Z c= Y implies Z in Tarski-Class X,(succ B) )
by A5, Th13;
A8:
succ B in A
by A2, A4, ORDINAL1:41;
assume A9:
( Z c= Y or Z = bool Y )
; Z in Tarski-Class X,A
thus
Z in Tarski-Class X,A
by A2, A6, A7, A8, A9, Th16; verum