let X, Y, 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, Th13;
A6:
bool Y in Tarski-Class (X,(succ B))
by A5, Th10;
A7:
( Z c= Y implies Z in Tarski-Class (X,(succ B)) )
by A5, Th10;
A8:
succ B in A
by A2, A4, ORDINAL1:28;
assume
( Z c= Y or Z = bool Y )
; Z in Tarski-Class (X,A)
hence
Z in Tarski-Class (X,A)
by A2, A6, A7, A8, Th13; verum