tarski_a.miz
begin
reserve x,y,z,u for
object;
reserve N,M,X,Y,Z for
set;
theorem ::
TARSKI_A:1
ex M st N
in M & (for X, Y holds X
in M & Y
c= X implies Y
in M) & (for X st X
in M holds ex Z st Z
in M & for Y st Y
c= X holds Y
in Z) & (for X holds X
c= M implies (X,M)
are_equipotent or X
in M);