 Tarski-Grothendieck set theory starts with conventional Zermelo-Fraenkel set theory and then adds “Tarski's axiom”.We will use the axioms, definitions, and notation of Mizar to describe it.Mizar's basic objects and processes are fully formal; they are described informally below.