:: Zermelo's Theorem
:: by Bogdan Nowak and S{\l}awomir Bia{\l}ecki
::
:: Received October 27, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: WELLSET1:1
theorem :: WELLSET1:2
canceled;
theorem Th3: :: WELLSET1:3
theorem :: WELLSET1:4
canceled;
theorem :: WELLSET1:5
canceled;
theorem Th6: :: WELLSET1:6
theorem Th7: :: WELLSET1:7
theorem Th8: :: WELLSET1:8
Lm1:
for X, M being set holds
( X,M are_equipotent iff ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) )
theorem :: WELLSET1:9