:: Tarski {G}rothendieck Set Theory -- Tarski's Axiom A
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

:: Alfred Tarski
:: Ueber unerreichbare Kardinalzahlen,
:: Fundamenta Mathematicae, vol. 30 (1938), pp. 68--69
:: Axiom A. (Axiom der unerreichbaren Mengen). Zu jeder Menge N gibt es
:: eine Menge M mit folgenden Eigenschaften:
:: A1. N in M;
:: A2. ist X in M und Y c= X, so ist Y in M;
:: A3. ist X in M und ist Z die Menge, die alle Mengen Y c= X und keine
:: andere Dinge als Element enthaelt, so,ist z in M;
:: A4. ist X c= M und sind dabei die Menge X und M nicht gleichmaechtig,
:: so ist X in M.
:: Alfred Tarski
:: On Well-ordered Subsets of any Set,
:: Fundamenta Mathematicae, vol. 32 (1939), pp. 176--183
:: A. For every set N there exists a system M of sets which satisfies
:: the following conditions:
:: (i) N in M
:: (ii) if X in M and Y c= X, then Y in M
:: (iii) if X in M and Z is the system of all subsets of X, then Z in M
:: (iv) if X c= M and X and M do not have the same potency, then X in M.
theorem :: TARSKI_A:1
for N being set ex M being set st
( N in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) & ( for X being set st X in M holds
ex Z being set st
( Z in M & ( for Y being set st Y c= X holds
Y in Z ) ) ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) ) ;