@MISC{TARSKI.MIZ,
  AUTHOR = {Trybulec, Andrzej},
  TITLE = {Tarski {G}rothendieck Set Theory},
  DAY = {01},
  MONTH = {January},
  YEAR = {1989},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {This is the first part of the axiomatics of the Mizar system. It includes
the axioms of the Tarski Grothendieck set theory. They are:
 the axiom stating that everything is a set,
 the extensionality axiom,
 the definitional axiom of the singleton,
 the definitional axiom of the pair,
 the definitional axiom of the union of a family of sets,
 the definitional axiom of the boolean (the power set) of a set,
 the regularity axiom,
 the definitional axiom of the ordered pair,
 the Tarski's axiom~A introduced in \cite{TARSKI:1} (see also \cite{TARSKI:2}),
 and the Fr\ae nkel scheme.
Also, the definition of equinumerosity is introduced.}}

