:: Zermelo's Theorem
::  by Bogdan Nowak and S{\l}awomir Bia{\l}ecki
::
:: Received October 27, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RELAT_1, FUNCT_1, XBOOLE_0, ZFMISC_1, SUBSET_1, WELLORD1,
      RELAT_2, TARSKI;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
      WELLORD1;
 constructors TARSKI, SUBSET_1, RELAT_2, WELLORD1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1;
 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
 for x being object holds
  x in field R iff ex y being object st ([x,y] in R or [y,x] in R);

theorem :: WELLSET1:2
  X <> {} & Y <> {} & W = [: X,Y :] implies field W = X \/ Y;

scheme :: WELLSET1:sch 1
  RSeparation { A()-> set, P[Relation] } :
  ex B st for R being Relation holds R in B iff R in A() & P[R];

theorem :: WELLSET1:3
  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:4
  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:5
  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:6
  for N ex R st R is well-ordering & field R = N;