Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Zermelo's Theorem

**by****Bogdan Nowak, and****Slawomir Bialecki**- Received October 27, 1989
- MML identifier: WELLSET1

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, FUNCT_1, BOOLE, WELLORD1, RELAT_2, TARSKI; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, WELLORD1; constructors TARSKI, RELAT_2, WELLORD1, SUBSET_1, XBOOLE_0; clusters RELAT_1, FUNCT_1, SUBSET_1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin reserve a,b,x,y,z,z1,z2,z3,y1,y3,y4,A,B,C,D,G,M,N,X,Y,Z,W0,W00 for set, R,S,T,W,W1,W2 for Relation, F,H,H1 for Function; theorem :: WELLSET1:1 x in field R iff ex y st ([x,y] in R or [y,x] in R); canceled; theorem :: WELLSET1:3 X <> {} & Y <> {} & W = [: X,Y :] implies field W = X \/ Y; scheme R_Separation { A()-> set, P[Relation] } : ex B st for R being Relation holds R in B iff R in A() & P[R]; canceled 2; theorem :: WELLSET1:6 for x,y,W st x in field W & y in field W & W is well-ordering holds not x in W-Seg(y) implies [y,x] in W; theorem :: WELLSET1:7 for x,y,W st x in field W & y in field W & W is well-ordering holds x in W-Seg(y) implies not [y,x] in W; theorem :: WELLSET1:8 for F,D st (for X st X in D holds not F.X in X & F.X in union D) ex R st field R c= union D & R is well-ordering & not field R in D & for y st y in field R holds R-Seg(y) in D & F.(R-Seg(y)) = y; theorem :: WELLSET1:9 for N ex R st R is well-ordering & field R = N;

Back to top