tarski_0.miz
begin
reserve x,y,z,a for
object;
reserve X,Y,Z for
set;
theorem ::
TARSKI_0:1
for x be
object holds x is
set;
theorem ::
TARSKI_0:2
(for x be
object holds x
in X iff x
in Y) implies X
= Y;
theorem ::
TARSKI_0:3
for x,y be
object holds ex z be
set st for a be
object holds a
in z iff a
= x or a
= y;
theorem ::
TARSKI_0:4
for X be
set holds ex Z be
set st for x be
object holds x
in Z iff ex Y be
set st x
in Y & Y
in X;
theorem ::
TARSKI_0:5
x
in X implies ex Y st Y
in X & not ex x st x
in X & x
in Y;
scheme ::
TARSKI_0:sch1
Replacement { A() ->
set , P[
object,
object] } :
ex X st for x holds x
in X iff ex y st y
in A() & P[y, x]
provided for x,y,z be
object st P[x, y] & P[x, z] holds y
= z;
thus thesis;
end;