theorem
for
X,
Y being
set st ( for
x being
element holds
(
x in X iff
x in Y ) ) holds
X = Y ;
theorem
for
x being
element for
X being
set st
x in X holds
ex
Y being
set st
(
Y in X & ( for
x being
element holds
( not
x in X or not
x in Y ) ) ) ;
theorem
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 ) ) ) ;
:: that any mathematical object that we need may be modelled in the set
:: theory.