@MISC{ZF_REFLE.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {The Reflection Theorem},
  DAY = {10},
  MONTH = {August},
  YEAR = {1990},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = { The goal is show that the reflection theorem holds. The
theorem is as usual in the Morse-Kelley theory of classes (MK).
That theory works with universal class which consists of all sets and
every class is a subclass of it. In this paper (and in another Mizar
articles) we work in Tarski-Grothendieck (TG)
theory (see \cite{TARSKI.ABS}) which ensures the existence
of sets that have properties like universal class (i.e. this theory is 
stronger than MK). The sets are introduced in \cite{CLASSES2.ABS}
and some concepts of MK are modeled.
The concepts are: the class $On$ of all ordinal numbers belonging
to the universe, subclasses, transfinite sequences of non-empty elements of
universe, etc.
The reflection theorem states that
 if $A_\xi$ is an increasing and continuous transfinite sequence of non-empty
sets and class $A = \bigcup_{\xi \in On} A_\xi$, then
for every formula $H$ there is a strictly increasing continuous mapping
 $F: On \to On$ such that if $\varkappa$ is a critical number of $F$
(i.e. $F(\varkappa) = \varkappa > 0$) and $f \in A_\varkappa^{\bf VAR}$, then
 $A,f\models H \equiv\ {A_\varkappa},f\models H$.
The proof is based on \cite{MOST:1}. Besides, in the article
it is shown that every universal class
is a model of ZF set theory if $\omega$ (the first infinite ordinal number)
belongs to it. Some propositions concerning ordinal numbers and sequences
of them are also present.}}

