:: ORDERS_1 semantic presentation

begin

            Lm1:  for Y being set holds
( ex X being set st
( X <> {} & X in Y ) iff union Y <> {} )
proof
let Y be set ; ::_thesis: ( ex X being set st
( X <> {} & X in Y ) iff union Y <> {} )
thus  ( ex X being set st
( X <> {} & X in Y ) implies union Y <> {} ) ::_thesis: ( union Y <> {} implies ex X being set st
( X <> {} & X in Y ) )
proof
given X being set  such that A1: X <> {} and
A2: X in Y ; ::_thesis: union Y <> {}
set x = the Element of X;
 the Element of X in X by A1;
hence  union Y <> {} by A2, TARSKI:def_4; ::_thesis: verum
end;
set x = the Element of union Y;
assume  union Y <> {} ; ::_thesis: ex X being set st
( X <> {} & X in Y )
then consider X being set  such that
A3: the Element of union Y in X and
A4: X in Y by TARSKI:def_4;
take  X ; ::_thesis: ( X <> {} & X in Y )
thus  ( X <> {} & X in Y ) by A3, A4; ::_thesis: verum
end;

definition
let M be non empty set ;
assume A1: not {} in M ;
mode Choice_Function of M ->  Function of M,(union M) means :Def1: :: ORDERS_1:def 1
 for X being set st X in M holds
it . X in X;
existence
 ex b1 being Function of M,(union M) st
for X being set st X in M holds
b1 . X in X
proof
deffunc H1( set ) ->  set = $1 `2 ;
set x = the Element of M;
deffunc H2( set ) ->  set = [:{$1},$1:];
consider f being Function such that
A2: dom f = M and
A3: for X being set st X in M holds
f . X = H2(X) from FUNCT_1:sch_3();
A4: the Element of M in M ;
then reconsider N = rng f as non empty set by A2, FUNCT_1:3;
A5: now__::_thesis:_for_X,_Y_being_set_st_X_in_N_&_Y_in_N_&_X_<>_Y_holds_
not_X_meets_Y
let X, Y be set ; ::_thesis: ( X in N & Y in N & X <> Y implies not X meets Y )
assume that
A6: X in N and
A7: Y in N and
A8: X <> Y ; ::_thesis: not X meets Y
consider y being set  such that
A9: y in dom f and
A10: f . y = Y by A7, FUNCT_1:def_3;
A11: Y = [:{y},y:] by A2, A3, A9, A10;
set z = the Element of X /\ Y;
assume  X meets Y ; ::_thesis: contradiction
then A12: X /\ Y <> {} by XBOOLE_0:def_7;
consider x being set  such that
A13: x in dom f and
A14: f . x = X by A6, FUNCT_1:def_3;
 X = [:{x},x:] by A2, A3, A13, A14;
then consider x1, x2 being set  such that
 the Element of X /\ Y = [x1,x2] and
A15: x1 in {x} /\ {y} and
 x2 in x /\ y by A11, A12, ZFMISC_1:85;
 x1 in {x} by A15, XBOOLE_0:def_4;
then A16: x1 = x by TARSKI:def_1;
 x1 in {y} by A15, XBOOLE_0:def_4;
hence  contradiction by A8, A14, A10, A16, TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_for_X_being_set_st_X_in_N_holds_
X_<>_{}
let X be set ; ::_thesis: ( X in N implies X <> {} )
assume  X in N ; ::_thesis: X <> {}
then consider y being set  such that
A17: y in dom f and
A18: f . y = X by FUNCT_1:def_3;
A19: y <> {} by A1, A2, A17;
 X = [:{y},y:] by A2, A3, A17, A18;
hence  X <> {} by A19; ::_thesis: verum
end;
then consider Choice being set  such that
A20: for X being set st X in N holds
ex x being set st Choice /\ X = {x} by A5, WELLORD2:18;
defpred S1[ set , set ] means $2 in $1 /\ Choice;
A21: for X being set st X in N holds
ex y being set st S1[X,y]
proof
let X be set ; ::_thesis: ( X in N implies ex y being set st S1[X,y] )
assume  X in N ; ::_thesis: ex y being set st S1[X,y]
then consider x being set  such that
A22: Choice /\ X = {x} by A20;
take  x ; ::_thesis: S1[X,x]
thus  S1[X,x] by A22, TARSKI:def_1; ::_thesis: verum
end;
A23: for X, y1, y2 being set st X in N & S1[X,y1] & S1[X,y2] holds
y1 = y2
proof
let X, y1, y2 be set ; ::_thesis: ( X in N & S1[X,y1] & S1[X,y2] implies y1 = y2 )
assume that
A24: X in N and
A25: y1 in X /\ Choice and
A26: y2 in X /\ Choice ; ::_thesis: y1 = y2
consider x being set  such that
A27: {x} = Choice /\ X by A20, A24;
 x = y1 by A25, A27, TARSKI:def_1;
hence  y1 = y2 by A26, A27, TARSKI:def_1; ::_thesis: verum
end;
consider g being Function such that
A28: dom g = N and
A29: for X being set st X in N holds
S1[X,g . X] from FUNCT_1:sch_2(A23, A21);
A30: rng g c= union N
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in union N )
assume  x in rng g ; ::_thesis: x in union N
then consider y being set  such that
A31: y in dom g and
A32: g . y = x by FUNCT_1:def_3;
 x in y /\ Choice by A28, A29, A31, A32;
then  x in y by XBOOLE_0:def_4;
hence  x in union N by A28, A31, TARSKI:def_4; ::_thesis: verum
end;
 f . the Element of M in rng f by A2, FUNCT_1:def_3;
then consider x1 being set  such that
A33: x1 in N ;
consider x2 being set  such that
A34: x2 in dom f and
A35: f . x2 = x1 by A33, FUNCT_1:def_3;
A36: x2 <> {} by A1, A2, A34;
reconsider f = f as Function of M,N by A2, FUNCT_2:def_1, RELSET_1:4;
consider h being Function such that
A37: dom h = union N and
A38: for x being set st x in union N holds
h . x = H1(x) from FUNCT_1:sch_3();
A39: rng h c= union M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng h or x in union M )
assume  x in rng h ; ::_thesis: x in union M
then consider y being set  such that
A40: y in dom h and
A41: h . y = x by FUNCT_1:def_3;
consider Y being set  such that
A42: y in Y and
A43: Y in N by A37, A40, TARSKI:def_4;
consider z being set  such that
A44: z in dom f and
A45: f . z = Y by A43, FUNCT_1:def_3;
A46: Y = [:{z},z:] by A3, A44, A45;
then consider x1, x2 being set  such that
A47: y = [x1,x2] by A42, RELAT_1:def_1;
A48: x2 in z by A42, A46, A47, ZFMISC_1:87;
 x = [x1,x2] `2 by A37, A38, A40, A41, A47;
then  x in z by A48;
hence  x in union M by A44, TARSKI:def_4; ::_thesis: verum
end;
 x1 = [:{x2},x2:] by A2, A3, A34, A35;
then A49: union N <> {} by A33, A36, Lm1;
then reconsider g = g as Function of N,(union N) by A28, A30, FUNCT_2:def_1, RELSET_1:4;
 union M <> {} by A1, A4, Lm1;
then reconsider h = h as Function of (union N),(union M) by A37, A39, FUNCT_2:def_1, RELSET_1:4;
A50: dom (g * f) = M by A49, FUNCT_2:def_1;
reconsider F = h * (g * f) as Function of M,(union M) by A49;
take  F ; ::_thesis: for X being set st X in M holds
F . X in X
let X be set ; ::_thesis: ( X in M implies F . X in X )
assume A51: X in M ; ::_thesis: F . X in X
then A52: f . X = [:{X},X:] by A3;
set fX = f . X;
A53: f . X in N by A2, A51, FUNCT_1:def_3;
then  g . (f . X) in rng g by A28, FUNCT_1:def_3;
then A54: h . (g . (f . X)) = (g . (f . X)) `2 by A38;
A55: g . (f . X) in (f . X) /\ Choice by A29, A53;
then consider x1, x2 being set  such that
A56: [x1,x2] = g . (f . X) by A52, RELAT_1:def_1;
 g . (f . X) in f . X by A55, XBOOLE_0:def_4;
then  x2 in X by A52, A56, ZFMISC_1:87;
then A57: h . (g . (f . X)) in X by A56, A54, MCART_1:7;
 (g * f) . X = g . (f . X) by A2, A51, FUNCT_1:13;
hence  F . X in X by A50, A51, A57, FUNCT_1:13; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Choice_Function ORDERS_1:def_1_:_
 for M being non empty set st not {} in M holds
for b2 being Function of M,(union M) holds
( b2 is Choice_Function of M iff for X being set st X in M holds
b2 . X in X );

definition
let D be set ;
func BOOL D ->  set  equals :: ORDERS_1:def 2
(bool D) \ {{}};
coherence
 (bool D) \ {{}} is set ;
end;

:: deftheorem  defines BOOL ORDERS_1:def_2_:_
 for D being set holds BOOL D = (bool D) \ {{}};

registration
let D be non empty set ;
cluster BOOL D ->  non empty ;
coherence
 not BOOL D is empty
proof
A1: not D in {{}} by TARSKI:def_1;
 D in bool D by ZFMISC_1:def_1;
hence  not BOOL D is empty by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem :: ORDERS_1:1
for D being non empty set holds not {} in BOOL D
proof
let D be non empty set ; ::_thesis: not {} in BOOL D
assume  {} in BOOL D ; ::_thesis: contradiction
then  not {} in {{}} by XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ORDERS_1:2
for X being set
for D being non empty set holds
( D c= X iff D in BOOL X )
proof
let X be set ; ::_thesis: for D being non empty set holds
( D c= X iff D in BOOL X )
let D be non empty set ; ::_thesis: ( D c= X iff D in BOOL X )
thus  ( D c= X implies D in BOOL X ) ::_thesis: ( D in BOOL X implies D c= X )
proof
A1: not D in {{}} by TARSKI:def_1;
assume  D c= X ; ::_thesis: D in BOOL X
hence  D in BOOL X by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
assume  D in BOOL X ; ::_thesis: D c= X
hence  D c= X ; ::_thesis: verum
end;

definition
let X be set ;
mode Order of X is reflexive antisymmetric transitive total Relation of X;
end;

 Lm2:  for X being set
for R being total Relation of X holds field R = X
proof
let X be set ; ::_thesis: for R being total Relation of X holds field R = X
let R be total Relation of X; ::_thesis: field R = X
thus  field R = X \/ (rng R) by PARTFUN1:def_2
.= X by XBOOLE_1:12 ; ::_thesis: verum
end;

theorem Th3: :: ORDERS_1:3
for X, x being set
for O being Order of X st x in X holds
[x,x] in O
proof
let X, x be set ; ::_thesis: for O being Order of X st x in X holds
[x,x] in O
let O be Order of X; ::_thesis: ( x in X implies [x,x] in O )
 field O = X by Lm2;
then  O is_reflexive_in X by RELAT_2:def_9;
hence  ( x in X implies [x,x] in O ) by RELAT_2:def_1; ::_thesis: verum
end;

theorem :: ORDERS_1:4
for X, x, y being set
for O being Order of X st x in X & y in X & [x,y] in O & [y,x] in O holds
x = y
proof
let X, x, y be set ; ::_thesis: for O being Order of X st x in X & y in X & [x,y] in O & [y,x] in O holds
x = y
let O be Order of X; ::_thesis: ( x in X & y in X & [x,y] in O & [y,x] in O implies x = y )
 field O = X by Lm2;
then  O is_antisymmetric_in X by RELAT_2:def_12;
hence  ( x in X & y in X & [x,y] in O & [y,x] in O implies x = y ) by RELAT_2:def_4; ::_thesis: verum
end;

theorem :: ORDERS_1:5
for X, x, y, z being set
for O being Order of X st x in X & y in X & z in X & [x,y] in O & [y,z] in O holds
[x,z] in O
proof
let X, x, y, z be set ; ::_thesis: for O being Order of X st x in X & y in X & z in X & [x,y] in O & [y,z] in O holds
[x,z] in O
let O be Order of X; ::_thesis: ( x in X & y in X & z in X & [x,y] in O & [y,z] in O implies [x,z] in O )
 field O = X by Lm2;
then  O is_transitive_in X by RELAT_2:def_16;
hence  ( x in X & y in X & z in X & [x,y] in O & [y,z] in O implies [x,z] in O ) by RELAT_2:def_8; ::_thesis: verum
end;

theorem :: ORDERS_1:6
for Y being set holds
( ex X being set st
( X <> {} & X in Y ) iff union Y <> {} ) by Lm1;

theorem :: ORDERS_1:7
for X being set
for P being Relation holds
( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) )
proof
let X be set ; ::_thesis: for P being Relation holds
( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) )
let P be Relation; ::_thesis: ( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) )
thus  ( P is_strongly_connected_in X implies ( P is_reflexive_in X & P is_connected_in X ) ) ::_thesis: ( P is_reflexive_in X & P is_connected_in X implies P is_strongly_connected_in X )
proof
assume A1: P is_strongly_connected_in X ; ::_thesis: ( P is_reflexive_in X & P is_connected_in X )
thus  P is_reflexive_in X ::_thesis: P is_connected_in X
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in P )
assume  x in X ; ::_thesis: [x,x] in P
hence  [x,x] in P by A1, RELAT_2:def_7; ::_thesis: verum
end;
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or x = b1 or [x,b1] in P or [b1,x] in P )
let y be set ; ::_thesis: ( not x in X or not y in X or x = y or [x,y] in P or [y,x] in P )
assume that
A2: x in X and
A3: y in X ; ::_thesis: ( x = y or [x,y] in P or [y,x] in P )
thus  ( x = y or [x,y] in P or [y,x] in P ) by A1, A2, A3, RELAT_2:def_7; ::_thesis: verum
end;
assume that
A4: P is_reflexive_in X and
A5: P is_connected_in X ; ::_thesis: P is_strongly_connected_in X
let x be set ; :: according to RELAT_2:def_7 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or [x,b1] in P or [b1,x] in P )
let y be set ; ::_thesis: ( not x in X or not y in X or [x,y] in P or [y,x] in P )
assume that
A6: x in X and
A7: y in X ; ::_thesis: ( [x,y] in P or [y,x] in P )
 ( x = y & not [x,y] in P implies [y,x] in P ) by A4, A6, RELAT_2:def_1;
hence  ( [x,y] in P or [y,x] in P ) by A5, A6, A7, RELAT_2:def_6; ::_thesis: verum
end;

theorem Th8: :: ORDERS_1:8
for X, Y being set
for P being Relation st P is_reflexive_in X & Y c= X holds
P is_reflexive_in Y
proof
let X, Y be set ; ::_thesis: for P being Relation st P is_reflexive_in X & Y c= X holds
P is_reflexive_in Y
let P be Relation; ::_thesis: ( P is_reflexive_in X & Y c= X implies P is_reflexive_in Y )
assume that
A1: P is_reflexive_in X and
A2: Y c= X ; ::_thesis: P is_reflexive_in Y
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in Y or [x,x] in P )
assume  x in Y ; ::_thesis: [x,x] in P
hence  [x,x] in P by A1, A2, RELAT_2:def_1; ::_thesis: verum
end;

theorem Th9: :: ORDERS_1:9
for X, Y being set
for P being Relation st P is_antisymmetric_in X & Y c= X holds
P is_antisymmetric_in Y
proof
let X, Y be set ; ::_thesis: for P being Relation st P is_antisymmetric_in X & Y c= X holds
P is_antisymmetric_in Y
let P be Relation; ::_thesis: ( P is_antisymmetric_in X & Y c= X implies P is_antisymmetric_in Y )
assume that
A1: P is_antisymmetric_in X and
A2: Y c= X ; ::_thesis: P is_antisymmetric_in Y
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds
( not x in Y or not b1 in Y or not [x,b1] in P or not [b1,x] in P or x = b1 )
let y be set ; ::_thesis: ( not x in Y or not y in Y or not [x,y] in P or not [y,x] in P or x = y )
assume that
A3: x in Y and
A4: y in Y ; ::_thesis: ( not [x,y] in P or not [y,x] in P or x = y )
thus  ( not [x,y] in P or not [y,x] in P or x = y ) by A1, A2, A3, A4, RELAT_2:def_4; ::_thesis: verum
end;

theorem Th10: :: ORDERS_1:10
for X, Y being set
for P being Relation st P is_transitive_in X & Y c= X holds
P is_transitive_in Y
proof
let X, Y be set ; ::_thesis: for P being Relation st P is_transitive_in X & Y c= X holds
P is_transitive_in Y
let P be Relation; ::_thesis: ( P is_transitive_in X & Y c= X implies P is_transitive_in Y )
assume that
A1: P is_transitive_in X and
A2: Y c= X ; ::_thesis: P is_transitive_in Y
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in Y or not b1 in Y or not b2 in Y or not [x,b1] in P or not [b1,b2] in P or [x,b2] in P )
let y, z be set ; ::_thesis: ( not x in Y or not y in Y or not z in Y or not [x,y] in P or not [y,z] in P or [x,z] in P )
assume that
A3: x in Y and
A4: y in Y and
A5: z in Y ; ::_thesis: ( not [x,y] in P or not [y,z] in P or [x,z] in P )
thus  ( not [x,y] in P or not [y,z] in P or [x,z] in P ) by A1, A2, A3, A4, A5, RELAT_2:def_8; ::_thesis: verum
end;

theorem :: ORDERS_1:11
for X, Y being set
for P being Relation st P is_strongly_connected_in X & Y c= X holds
P is_strongly_connected_in Y
proof
let X, Y be set ; ::_thesis: for P being Relation st P is_strongly_connected_in X & Y c= X holds
P is_strongly_connected_in Y
let P be Relation; ::_thesis: ( P is_strongly_connected_in X & Y c= X implies P is_strongly_connected_in Y )
assume that
A1: P is_strongly_connected_in X and
A2: Y c= X ; ::_thesis: P is_strongly_connected_in Y
let x be set ; :: according to RELAT_2:def_7 ::_thesis: for b1 being set holds
( not x in Y or not b1 in Y or [x,b1] in P or [b1,x] in P )
let y be set ; ::_thesis: ( not x in Y or not y in Y or [x,y] in P or [y,x] in P )
assume that
A3: x in Y and
A4: y in Y ; ::_thesis: ( [x,y] in P or [y,x] in P )
thus  ( [x,y] in P or [y,x] in P ) by A1, A2, A3, A4, RELAT_2:def_7; ::_thesis: verum
end;

theorem :: ORDERS_1:12
for X being set
for R being total Relation of X holds field R = X by Lm2;

theorem Th13: :: ORDERS_1:13
for A being set
for R being Relation of A st R is_reflexive_in A holds
( dom R = A & field R = A )
proof
let A be set ; ::_thesis: for R being Relation of A st R is_reflexive_in A holds
( dom R = A & field R = A )
let R be Relation of A; ::_thesis: ( R is_reflexive_in A implies ( dom R = A & field R = A ) )
assume A1: R is_reflexive_in A ; ::_thesis: ( dom R = A & field R = A )
A2: A c= dom R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in dom R )
assume  x in A ; ::_thesis: x in dom R
then  [x,x] in R by A1, RELAT_2:def_1;
hence  x in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;
hence  dom R = A by XBOOLE_0:def_10; ::_thesis: field R = A
thus  field R = A \/ (rng R) by A2, XBOOLE_0:def_10
.= A by XBOOLE_1:12 ; ::_thesis: verum
end;

begin


theorem Th14: :: ORDERS_1:14
for X being set
for O being Order of X holds
( dom O = X & rng O = X )
proof
let X be set ; ::_thesis: for O being Order of X holds
( dom O = X & rng O = X )
let O be Order of X; ::_thesis: ( dom O = X & rng O = X )
thus  dom O = X ::_thesis: rng O = X
proof
thus  dom O c= X ; :: according to XBOOLE_0:def_10 ::_thesis: X c= dom O
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom O )
assume  x in X ; ::_thesis: x in dom O
then  [x,x] in O by Th3;
hence  x in dom O by XTUPLE_0:def_12; ::_thesis: verum
end;
thus  rng O c= X ; :: according to XBOOLE_0:def_10 ::_thesis: X c= rng O
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in rng O )
assume  x in X ; ::_thesis: x in rng O
then  [x,x] in O by Th3;
hence  x in rng O by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: ORDERS_1:15
for X being set
for O being Order of X holds field O = X
proof
let X be set ; ::_thesis: for O being Order of X holds field O = X
let O be Order of X; ::_thesis: field O = X
thus X = X \/ X
.= (dom O) \/ X by Th14
.= field O by Th14 ; ::_thesis: verum
end;

definition
let R be Relation;
attrR is being_quasi-order  means :: ORDERS_1:def 3
( R is reflexive & R is transitive );
attrR is being_partial-order  means :Def4: :: ORDERS_1:def 4
( R is reflexive & R is transitive & R is antisymmetric );
attrR is being_linear-order  means :Def5: :: ORDERS_1:def 5
( R is reflexive & R is transitive & R is antisymmetric & R is connected );
end;

:: deftheorem  defines being_quasi-order ORDERS_1:def_3_:_
 for R being Relation holds
( R is being_quasi-order iff ( R is reflexive & R is transitive ) );

:: deftheorem Def4 defines being_partial-order ORDERS_1:def_4_:_
 for R being Relation holds
( R is being_partial-order iff ( R is reflexive & R is transitive & R is antisymmetric ) );

:: deftheorem Def5 defines being_linear-order ORDERS_1:def_5_:_
 for R being Relation holds
( R is being_linear-order iff ( R is reflexive & R is transitive & R is antisymmetric & R is connected ) );

theorem :: ORDERS_1:16
for R being Relation st R is being_quasi-order holds
R ~ is being_quasi-order
proof
let R be Relation; ::_thesis: ( R is being_quasi-order implies R ~ is being_quasi-order )
assume that
A1: R is reflexive and
A2: R is transitive ; :: according to ORDERS_1:def_3 ::_thesis: R ~ is being_quasi-order
thus  ( R ~ is reflexive & R ~ is transitive ) by A1, A2; :: according to ORDERS_1:def_3 ::_thesis: verum
end;

theorem :: ORDERS_1:17
for R being Relation st R is being_partial-order holds
R ~ is being_partial-order
proof
let R be Relation; ::_thesis: ( R is being_partial-order implies R ~ is being_partial-order )
assume that
A1: R is reflexive and
A2: R is transitive and
A3: R is antisymmetric ; :: according to ORDERS_1:def_4 ::_thesis: R ~ is being_partial-order
thus  ( R ~ is reflexive & R ~ is transitive & R ~ is antisymmetric ) by A1, A2, A3; :: according to ORDERS_1:def_4 ::_thesis: verum
end;

Lm3:  for R being Relation st R is connected holds
R ~ is connected
proof
let R be Relation; ::_thesis: ( R is connected implies R ~ is connected )
assume A1: for x, y being set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: R ~ is connected
let x be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds
( not x in field (R ~) or not b1 in field (R ~) or x = b1 or [x,b1] in R ~ or [b1,x] in R ~ )
let y be set ; ::_thesis: ( not x in field (R ~) or not y in field (R ~) or x = y or [x,y] in R ~ or [y,x] in R ~ )
assume that
A2: x in field (R ~) and
A3: y in field (R ~) and
A4: x <> y ; ::_thesis: ( [x,y] in R ~ or [y,x] in R ~ )
 field R = field (R ~) by RELAT_1:21;
then  ( [x,y] in R or [y,x] in R ) by A1, A2, A3, A4;
hence  ( [x,y] in R ~ or [y,x] in R ~ ) by RELAT_1:def_7; ::_thesis: verum
end;

theorem Th18: :: ORDERS_1:18
for R being Relation st R is being_linear-order holds
R ~ is being_linear-order
proof
let R be Relation; ::_thesis: ( R is being_linear-order implies R ~ is being_linear-order )
assume that
A1: R is reflexive and
A2: R is transitive and
A3: R is antisymmetric and
A4: R is connected ; :: according to ORDERS_1:def_5 ::_thesis: R ~ is being_linear-order
thus  ( R ~ is reflexive & R ~ is transitive & R ~ is antisymmetric & R ~ is connected ) by A1, A2, A3, A4, Lm3; :: according to ORDERS_1:def_5 ::_thesis: verum
end;

theorem :: ORDERS_1:19
for R being Relation st R is well-ordering holds
( R is being_quasi-order & R is being_partial-order & R is being_linear-order )
proof
let R be Relation; ::_thesis: ( R is well-ordering implies ( R is being_quasi-order & R is being_partial-order & R is being_linear-order ) )
assume that
A1: R is reflexive and
A2: R is transitive and
A3: R is antisymmetric and
A4: R is connected and
 R is well_founded ; :: according to WELLORD1:def_4 ::_thesis: ( R is being_quasi-order & R is being_partial-order & R is being_linear-order )
thus  ( R is reflexive & R is transitive & R is reflexive & R is transitive & R is antisymmetric & R is reflexive & R is transitive & R is antisymmetric & R is connected ) by A1, A2, A3, A4; :: according to ORDERS_1:def_3,ORDERS_1:def_4,ORDERS_1:def_5 ::_thesis: verum
end;

theorem :: ORDERS_1:20
for R being Relation st R is being_linear-order holds
( R is being_quasi-order & R is being_partial-order )
proof
let R be Relation; ::_thesis: ( R is being_linear-order implies ( R is being_quasi-order & R is being_partial-order ) )
assume that
A1: R is reflexive and
A2: R is transitive and
A3: R is antisymmetric and
 R is connected ; :: according to ORDERS_1:def_5 ::_thesis: ( R is being_quasi-order & R is being_partial-order )
thus  ( R is reflexive & R is transitive & R is reflexive & R is transitive & R is antisymmetric ) by A1, A2, A3; :: according to ORDERS_1:def_3,ORDERS_1:def_4 ::_thesis: verum
end;

theorem Th21: :: ORDERS_1:21
for R being Relation st R is being_partial-order holds
R is being_quasi-order
proof
let R be Relation; ::_thesis: ( R is being_partial-order implies R is being_quasi-order )
assume that
A1: R is reflexive and
A2: R is transitive and
 R is antisymmetric ; :: according to ORDERS_1:def_4 ::_thesis: R is being_quasi-order
thus  ( R is reflexive & R is transitive ) by A1, A2; :: according to ORDERS_1:def_3 ::_thesis: verum
end;

theorem :: ORDERS_1:22
for X being set
for O being Order of X holds O is being_partial-order by Def4;

theorem :: ORDERS_1:23
for X being set
for O being Order of X holds O is being_quasi-order
proof
let X be set ; ::_thesis: for O being Order of X holds O is being_quasi-order
let O be Order of X; ::_thesis: O is being_quasi-order
 O is being_partial-order by Def4;
hence  O is being_quasi-order by Th21; ::_thesis: verum
end;

theorem :: ORDERS_1:24
for X being set
for O being Order of X st O is connected holds
O is being_linear-order by Def5;

Lm4:  for R being Relation holds R c= [:(field R),(field R):]
proof
let R be Relation; ::_thesis: R c= [:(field R),(field R):]
let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [y,b1] in R or [y,b1] in [:(field R),(field R):] )
let z be set ; ::_thesis: ( not [y,z] in R or [y,z] in [:(field R),(field R):] )
assume A1: [y,z] in R ; ::_thesis: [y,z] in [:(field R),(field R):]
then A2: z in field R by RELAT_1:15;
 y in field R by A1, RELAT_1:15;
hence  [y,z] in [:(field R),(field R):] by A2, ZFMISC_1:87; ::_thesis: verum
end;

Lm5:  for R being Relation
for X being set st R is reflexive & X c= field R holds
field (R |_2 X) = X
proof
let R be Relation; ::_thesis: for X being set st R is reflexive & X c= field R holds
field (R |_2 X) = X
let X be set ; ::_thesis: ( R is reflexive & X c= field R implies field (R |_2 X) = X )
assume that
A1: for x being set st x in field R holds
[x,x] in R and
A2: X c= field R ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: field (R |_2 X) = X
thus  field (R |_2 X) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= field (R |_2 X)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in field (R |_2 X) or y in X )
thus  ( not y in field (R |_2 X) or y in X ) by WELLORD1:12; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in field (R |_2 X) )
assume A3: y in X ; ::_thesis: y in field (R |_2 X)
then A4: [y,y] in [:X,X:] by ZFMISC_1:87;
 [y,y] in R by A1, A2, A3;
then  [y,y] in R |_2 X by A4, XBOOLE_0:def_4;
hence  y in field (R |_2 X) by RELAT_1:15; ::_thesis: verum
end;

theorem :: ORDERS_1:25
for R being Relation
for X being set st R is being_quasi-order holds
R |_2 X is being_quasi-order
proof
let R be Relation; ::_thesis: for X being set st R is being_quasi-order holds
R |_2 X is being_quasi-order
let X be set ; ::_thesis: ( R is being_quasi-order implies R |_2 X is being_quasi-order )
assume that
A1: R is reflexive and
A2: R is transitive ; :: according to ORDERS_1:def_3 ::_thesis: R |_2 X is being_quasi-order
thus  ( R |_2 X is reflexive & R |_2 X is transitive ) by A1, A2, WELLORD1:15, WELLORD1:17; :: according to ORDERS_1:def_3 ::_thesis: verum
end;

theorem :: ORDERS_1:26
for R being Relation
for X being set st R is being_partial-order holds
R |_2 X is being_partial-order
proof
let R be Relation; ::_thesis: for X being set st R is being_partial-order holds
R |_2 X is being_partial-order
let X be set ; ::_thesis: ( R is being_partial-order implies R |_2 X is being_partial-order )
assume that
A1: R is reflexive and
A2: R is transitive and
A3: R is antisymmetric ; :: according to ORDERS_1:def_4 ::_thesis: R |_2 X is being_partial-order
thus  ( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric ) by A1, A2, A3, WELLORD1:15, WELLORD1:17; :: according to ORDERS_1:def_4 ::_thesis: verum
end;

theorem :: ORDERS_1:27
for R being Relation
for X being set st R is being_linear-order holds
R |_2 X is being_linear-order
proof
let R be Relation; ::_thesis: for X being set st R is being_linear-order holds
R |_2 X is being_linear-order
let X be set ; ::_thesis: ( R is being_linear-order implies R |_2 X is being_linear-order )
assume that
A1: R is reflexive and
A2: R is transitive and
A3: R is antisymmetric and
A4: R is connected ; :: according to ORDERS_1:def_5 ::_thesis: R |_2 X is being_linear-order
thus  ( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric & R |_2 X is connected ) by A1, A2, A3, A4, WELLORD1:15, WELLORD1:16, WELLORD1:17; :: according to ORDERS_1:def_5 ::_thesis: verum
end;

registration
let R be empty Relation;
cluster field R ->  empty ;
coherence
 field R is empty ;
end;

registration
cluster empty Relation-like  ->  well-ordering being_quasi-order being_partial-order being_linear-order for set ;
coherence
 for b1 being Relation st b1 is empty holds
( b1 is being_quasi-order & b1 is being_partial-order & b1 is being_linear-order & b1 is well-ordering )
proof
let R be Relation; ::_thesis: ( R is empty implies ( R is being_quasi-order & R is being_partial-order & R is being_linear-order & R is well-ordering ) )
assume A1: R is empty ; ::_thesis: ( R is being_quasi-order & R is being_partial-order & R is being_linear-order & R is well-ordering )
thus A2: R is reflexive :: according to ORDERS_1:def_3 ::_thesis: ( R is transitive & R is being_partial-order & R is being_linear-order & R is well-ordering )
proof
let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field R or [x,x] in R )
assume  x in field R ; ::_thesis: [x,x] in R
hence  [x,x] in R by A1; ::_thesis: verum
end;
thus A3: R is transitive ::_thesis: ( R is being_partial-order & R is being_linear-order & R is well-ordering )
proof
let x be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for b1, b2 being set holds
( not x in field R or not b1 in field R or not b2 in field R or not [x,b1] in R or not [b1,b2] in R or [x,b2] in R )
let y, z be set ; ::_thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume  x in field R ; ::_thesis: ( not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )
thus  ( not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R ) by A1; ::_thesis: verum
end;
hence  ( R is reflexive & R is transitive ) by A2; :: according to ORDERS_1:def_4 ::_thesis: ( R is antisymmetric & R is being_linear-order & R is well-ordering )
thus A4: R is antisymmetric ::_thesis: ( R is being_linear-order & R is well-ordering )
proof
let x be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for b1 being set holds
( not x in field R or not b1 in field R or not [x,b1] in R or not [b1,x] in R or x = b1 )
let y be set ; ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R or x = y )
assume  x in field R ; ::_thesis: ( not y in field R or not [x,y] in R or not [y,x] in R or x = y )
thus  ( not y in field R or not [x,y] in R or not [y,x] in R or x = y ) by A1; ::_thesis: verum
end;
hence  ( R is reflexive & R is transitive & R is antisymmetric ) by A2, A3; :: according to ORDERS_1:def_5 ::_thesis: ( R is connected & R is well-ordering )
thus  R is connected ::_thesis: R is well-ordering
proof
let x be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds
( not x in field R or not b1 in field R or x = b1 or [x,b1] in R or [b1,x] in R )
let y be set ; ::_thesis: ( not x in field R or not y in field R or x = y or [x,y] in R or [y,x] in R )
assume  x in field R ; ::_thesis: ( not y in field R or x = y or [x,y] in R or [y,x] in R )
thus  ( not y in field R or x = y or [x,y] in R or [y,x] in R ) by A1; ::_thesis: verum
end;
hence  ( R is reflexive & R is transitive & R is antisymmetric & R is connected ) by A2, A3, A4; :: according to WELLORD1:def_4 ::_thesis: R is well_founded
let Y be set ; :: according to WELLORD1:def_2 ::_thesis: ( not Y c= field R or Y = {} or ex b1 being set st
( b1 in Y & R -Seg b1 misses Y ) )
assume that
A5: Y c= field R and
A6: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & R -Seg b1 misses Y )
thus  ex b1 being set st
( b1 in Y & R -Seg b1 misses Y ) by A5, A6, A1; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster id X ->  being_quasi-order being_partial-order ;
coherence
 ( id X is being_quasi-order & id X is being_partial-order )
proof
thus  ( id X is reflexive & id X is transitive & id X is reflexive & id X is transitive & id X is antisymmetric ) ; :: according to ORDERS_1:def_3,ORDERS_1:def_4 ::_thesis: verum
end;
end;

definition
let R be Relation;
let X be set ;
predR quasi_orders X means :Def6: :: ORDERS_1:def 6
( R is_reflexive_in X & R is_transitive_in X );
predR partially_orders X means :Def7: :: ORDERS_1:def 7
( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X );
predR linearly_orders X means :: ORDERS_1:def 8
( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X );
end;

:: deftheorem Def6 defines quasi_orders ORDERS_1:def_6_:_
 for R being Relation
for X being set holds
( R quasi_orders X iff ( R is_reflexive_in X & R is_transitive_in X ) );

:: deftheorem Def7 defines partially_orders ORDERS_1:def_7_:_
 for R being Relation
for X being set holds
( R partially_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ) );

:: deftheorem  defines linearly_orders ORDERS_1:def_8_:_
 for R being Relation
for X being set holds
( R linearly_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ) );

theorem Th28: :: ORDERS_1:28
for R being Relation
for X being set st R well_orders X holds
( R quasi_orders X & R partially_orders X & R linearly_orders X )
proof
let R be Relation; ::_thesis: for X being set st R well_orders X holds
( R quasi_orders X & R partially_orders X & R linearly_orders X )
let X be set ; ::_thesis: ( R well_orders X implies ( R quasi_orders X & R partially_orders X & R linearly_orders X ) )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X and
A3: R is_antisymmetric_in X and
A4: R is_connected_in X and
 R is_well_founded_in X ; :: according to WELLORD1:def_5 ::_thesis: ( R quasi_orders X & R partially_orders X & R linearly_orders X )
thus  ( R is_reflexive_in X & R is_transitive_in X & R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ) by A1, A2, A3, A4; :: according to ORDERS_1:def_6,ORDERS_1:def_7,ORDERS_1:def_8 ::_thesis: verum
end;

theorem Th29: :: ORDERS_1:29
for R being Relation
for X being set st R linearly_orders X holds
( R quasi_orders X & R partially_orders X )
proof
let R be Relation; ::_thesis: for X being set st R linearly_orders X holds
( R quasi_orders X & R partially_orders X )
let X be set ; ::_thesis: ( R linearly_orders X implies ( R quasi_orders X & R partially_orders X ) )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X and
A3: R is_antisymmetric_in X and
 R is_connected_in X ; :: according to ORDERS_1:def_8 ::_thesis: ( R quasi_orders X & R partially_orders X )
thus  ( R is_reflexive_in X & R is_transitive_in X & R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ) by A1, A2, A3; :: according to ORDERS_1:def_6,ORDERS_1:def_7 ::_thesis: verum
end;

theorem :: ORDERS_1:30
for R being Relation
for X being set st R partially_orders X holds
R quasi_orders X
proof
let R be Relation; ::_thesis: for X being set st R partially_orders X holds
R quasi_orders X
let X be set ; ::_thesis: ( R partially_orders X implies R quasi_orders X )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X and
 R is_antisymmetric_in X ; :: according to ORDERS_1:def_7 ::_thesis: R quasi_orders X
thus  ( R is_reflexive_in X & R is_transitive_in X ) by A1, A2; :: according to ORDERS_1:def_6 ::_thesis: verum
end;

theorem Th31: :: ORDERS_1:31
for R being Relation st R is being_quasi-order holds
R quasi_orders field R
proof
let R be Relation; ::_thesis: ( R is being_quasi-order implies R quasi_orders field R )
assume that
A1: R is_reflexive_in field R and
A2: R is_transitive_in field R ; :: according to RELAT_2:def_9,RELAT_2:def_16,ORDERS_1:def_3 ::_thesis: R quasi_orders field R
thus  ( R is_reflexive_in field R & R is_transitive_in field R ) by A1, A2; :: according to ORDERS_1:def_6 ::_thesis: verum
end;

theorem :: ORDERS_1:32
for R being Relation
for Y, X being set st R quasi_orders Y & X c= Y holds
R quasi_orders X
proof
let R be Relation; ::_thesis: for Y, X being set st R quasi_orders Y & X c= Y holds
R quasi_orders X
let Y, X be set ; ::_thesis: ( R quasi_orders Y & X c= Y implies R quasi_orders X )
assume that
A1: R is_reflexive_in Y and
A2: R is_transitive_in Y and
A3: X c= Y ; :: according to ORDERS_1:def_6 ::_thesis: R quasi_orders X
thus  ( R is_reflexive_in X & R is_transitive_in X ) by A1, A2, A3, Th8, Th10; :: according to ORDERS_1:def_6 ::_thesis: verum
end;

Lm6:  for R being Relation
for X being set st R is_reflexive_in X holds
R |_2 X is reflexive
proof
let R be Relation; ::_thesis: for X being set st R is_reflexive_in X holds
R |_2 X is reflexive
let X be set ; ::_thesis: ( R is_reflexive_in X implies R |_2 X is reflexive )
assume A1: for x being set st x in X holds
[x,x] in R ; :: according to RELAT_2:def_1 ::_thesis: R |_2 X is reflexive
let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field (R |_2 X) or [x,x] in R |_2 X )
assume A2: x in field (R |_2 X) ; ::_thesis: [x,x] in R |_2 X
then  x in X by WELLORD1:12;
then A3: [x,x] in [:X,X:] by ZFMISC_1:87;
 [x,x] in R by A1, A2, WELLORD1:12;
hence  [x,x] in R |_2 X by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

Lm7:  for R being Relation
for X being set st R is_transitive_in X holds
R |_2 X is transitive
proof
let R be Relation; ::_thesis: for X being set st R is_transitive_in X holds
R |_2 X is transitive
let X be set ; ::_thesis: ( R is_transitive_in X implies R |_2 X is transitive )
assume A1: for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds
[x,z] in R ; :: according to RELAT_2:def_8 ::_thesis: R |_2 X is transitive
let x be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for b1, b2 being set holds
( not x in field (R |_2 X) or not b1 in field (R |_2 X) or not b2 in field (R |_2 X) or not [x,b1] in R |_2 X or not [b1,b2] in R |_2 X or [x,b2] in R |_2 X )
let y, z be set ; ::_thesis: ( not x in field (R |_2 X) or not y in field (R |_2 X) or not z in field (R |_2 X) or not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X )
assume that
A2: x in field (R |_2 X) and
A3: y in field (R |_2 X) and
A4: z in field (R |_2 X) ; ::_thesis: ( not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X )
A5: z in X by A4, WELLORD1:12;
A6: x in X by A2, WELLORD1:12;
then A7: [x,z] in [:X,X:] by A5, ZFMISC_1:87;
assume that
A8: [x,y] in R |_2 X and
A9: [y,z] in R |_2 X ; ::_thesis: [x,z] in R |_2 X
A10: [x,y] in R by A8, XBOOLE_0:def_4;
A11: [y,z] in R by A9, XBOOLE_0:def_4;
 y in X by A3, WELLORD1:12;
then  [x,z] in R by A1, A6, A5, A10, A11;
hence  [x,z] in R |_2 X by A7, XBOOLE_0:def_4; ::_thesis: verum
end;

Lm8:  for R being Relation
for X being set st R is_antisymmetric_in X holds
R |_2 X is antisymmetric
proof
let R be Relation; ::_thesis: for X being set st R is_antisymmetric_in X holds
R |_2 X is antisymmetric
let X be set ; ::_thesis: ( R is_antisymmetric_in X implies R |_2 X is antisymmetric )
assume A1: for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y ; :: according to RELAT_2:def_4 ::_thesis: R |_2 X is antisymmetric
let x be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for b1 being set holds
( not x in field (R |_2 X) or not b1 in field (R |_2 X) or not [x,b1] in R |_2 X or not [b1,x] in R |_2 X or x = b1 )
let y be set ; ::_thesis: ( not x in field (R |_2 X) or not y in field (R |_2 X) or not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y )
assume that
A2: x in field (R |_2 X) and
A3: y in field (R |_2 X) ; ::_thesis: ( not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y )
A4: y in X by A3, WELLORD1:12;
assume that
A5: [x,y] in R |_2 X and
A6: [y,x] in R |_2 X ; ::_thesis: x = y
A7: [x,y] in R by A5, XBOOLE_0:def_4;
A8: [y,x] in R by A6, XBOOLE_0:def_4;
 x in X by A2, WELLORD1:12;
hence  x = y by A1, A4, A7, A8; ::_thesis: verum
end;

Lm9:  for R being Relation
for X being set st R is_connected_in X holds
R |_2 X is connected
proof
let R be Relation; ::_thesis: for X being set st R is_connected_in X holds
R |_2 X is connected
let X be set ; ::_thesis: ( R is_connected_in X implies R |_2 X is connected )
assume A1: for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds
[y,x] in R ; :: according to RELAT_2:def_6 ::_thesis: R |_2 X is connected
let x be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds
( not x in field (R |_2 X) or not b1 in field (R |_2 X) or x = b1 or [x,b1] in R |_2 X or [b1,x] in R |_2 X )
let y be set ; ::_thesis: ( not x in field (R |_2 X) or not y in field (R |_2 X) or x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
assume that
A2: x in field (R |_2 X) and
A3: y in field (R |_2 X) and
A4: x <> y ; ::_thesis: ( [x,y] in R |_2 X or [y,x] in R |_2 X )
A5: y in X by A3, WELLORD1:12;
A6: x in X by A2, WELLORD1:12;
then A7: [x,y] in [:X,X:] by A5, ZFMISC_1:87;
A8: [y,x] in [:X,X:] by A6, A5, ZFMISC_1:87;
 ( [x,y] in R or [y,x] in R ) by A1, A4, A6, A5;
hence  ( [x,y] in R |_2 X or [y,x] in R |_2 X ) by A7, A8, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: ORDERS_1:33
for R being Relation
for X being set st R quasi_orders X holds
R |_2 X is being_quasi-order
proof
let R be Relation; ::_thesis: for X being set st R quasi_orders X holds
R |_2 X is being_quasi-order
let X be set ; ::_thesis: ( R quasi_orders X implies R |_2 X is being_quasi-order )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X ; :: according to ORDERS_1:def_6 ::_thesis: R |_2 X is being_quasi-order
thus  ( R |_2 X is reflexive & R |_2 X is transitive ) by A1, A2, Lm6, Lm7; :: according to ORDERS_1:def_3 ::_thesis: verum
end;

theorem Th34: :: ORDERS_1:34
for R being Relation st R is being_partial-order holds
R partially_orders field R
proof
let R be Relation; ::_thesis: ( R is being_partial-order implies R partially_orders field R )
assume that
A1: R is_reflexive_in field R and
A2: R is_transitive_in field R and
A3: R is_antisymmetric_in field R ; :: according to RELAT_2:def_9,RELAT_2:def_12,RELAT_2:def_16,ORDERS_1:def_4 ::_thesis: R partially_orders field R
thus  ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R ) by A1, A2, A3; :: according to ORDERS_1:def_7 ::_thesis: verum
end;

theorem :: ORDERS_1:35
for R being Relation
for Y, X being set st R partially_orders Y & X c= Y holds
R partially_orders X
proof
let R be Relation; ::_thesis: for Y, X being set st R partially_orders Y & X c= Y holds
R partially_orders X
let Y, X be set ; ::_thesis: ( R partially_orders Y & X c= Y implies R partially_orders X )
assume that
A1: R is_reflexive_in Y and
A2: R is_transitive_in Y and
A3: R is_antisymmetric_in Y and
A4: X c= Y ; :: according to ORDERS_1:def_7 ::_thesis: R partially_orders X
thus  ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ) by A1, A2, A3, A4, Th8, Th9, Th10; :: according to ORDERS_1:def_7 ::_thesis: verum
end;

theorem :: ORDERS_1:36
for R being Relation
for X being set st R partially_orders X holds
R |_2 X is being_partial-order
proof
let R be Relation; ::_thesis: for X being set st R partially_orders X holds
R |_2 X is being_partial-order
let X be set ; ::_thesis: ( R partially_orders X implies R |_2 X is being_partial-order )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X and
A3: R is_antisymmetric_in X ; :: according to ORDERS_1:def_7 ::_thesis: R |_2 X is being_partial-order
thus  ( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric ) by A1, A2, A3, Lm6, Lm7, Lm8; :: according to ORDERS_1:def_4 ::_thesis: verum
end;

Lm10:  for R being Relation
for X, Y being set st R is_connected_in X & Y c= X holds
R is_connected_in Y
proof
let R be Relation; ::_thesis: for X, Y being set st R is_connected_in X & Y c= X holds
R is_connected_in Y
let X, Y be set ; ::_thesis: ( R is_connected_in X & Y c= X implies R is_connected_in Y )
assume that
A1: R is_connected_in X and
A2: Y c= X ; ::_thesis: R is_connected_in Y
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in Y or not b1 in Y or x = b1 or [x,b1] in R or [b1,x] in R )
let y be set ; ::_thesis: ( not x in Y or not y in Y or x = y or [x,y] in R or [y,x] in R )
assume that
A3: x in Y and
A4: y in Y ; ::_thesis: ( x = y or [x,y] in R or [y,x] in R )
thus  ( x = y or [x,y] in R or [y,x] in R ) by A1, A2, A3, A4, RELAT_2:def_6; ::_thesis: verum
end;

theorem :: ORDERS_1:37
for R being Relation st R is being_linear-order holds
R linearly_orders field R
proof
let R be Relation; ::_thesis: ( R is being_linear-order implies R linearly_orders field R )
assume that
A1: R is_reflexive_in field R and
A2: R is_transitive_in field R and
A3: R is_antisymmetric_in field R and
A4: R is_connected_in field R ; :: according to RELAT_2:def_9,RELAT_2:def_12,RELAT_2:def_14,RELAT_2:def_16,ORDERS_1:def_5 ::_thesis: R linearly_orders field R
thus  ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R & R is_connected_in field R ) by A1, A2, A3, A4; :: according to ORDERS_1:def_8 ::_thesis: verum
end;

theorem :: ORDERS_1:38
for R being Relation
for Y, X being set st R linearly_orders Y & X c= Y holds
R linearly_orders X
proof
let R be Relation; ::_thesis: for Y, X being set st R linearly_orders Y & X c= Y holds
R linearly_orders X
let Y, X be set ; ::_thesis: ( R linearly_orders Y & X c= Y implies R linearly_orders X )
assume that
A1: R is_reflexive_in Y and
A2: R is_transitive_in Y and
A3: R is_antisymmetric_in Y and
A4: R is_connected_in Y and
A5: X c= Y ; :: according to ORDERS_1:def_8 ::_thesis: R linearly_orders X
thus  ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ) by A1, A2, A3, A4, A5, Lm10, Th8, Th9, Th10; :: according to ORDERS_1:def_8 ::_thesis: verum
end;

theorem :: ORDERS_1:39
for R being Relation
for X being set st R linearly_orders X holds
R |_2 X is being_linear-order
proof
let R be Relation; ::_thesis: for X being set st R linearly_orders X holds
R |_2 X is being_linear-order
let X be set ; ::_thesis: ( R linearly_orders X implies R |_2 X is being_linear-order )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X and
A3: R is_antisymmetric_in X and
A4: R is_connected_in X ; :: according to ORDERS_1:def_8 ::_thesis: R |_2 X is being_linear-order
thus  ( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric & R |_2 X is connected ) by A1, A2, A3, A4, Lm6, Lm7, Lm8, Lm9; :: according to ORDERS_1:def_5 ::_thesis: verum
end;

Lm11:  for R being Relation
for X being set st R is_reflexive_in X holds
R ~ is_reflexive_in X
proof
let R be Relation; ::_thesis: for X being set st R is_reflexive_in X holds
R ~ is_reflexive_in X
let X be set ; ::_thesis: ( R is_reflexive_in X implies R ~ is_reflexive_in X )
assume A1: for x being set st x in X holds
[x,x] in R ; :: according to RELAT_2:def_1 ::_thesis: R ~ is_reflexive_in X
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in R ~ )
assume  x in X ; ::_thesis: [x,x] in R ~
then  [x,x] in R by A1;
hence  [x,x] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;

Lm12:  for R being Relation
for X being set st R is_transitive_in X holds
R ~ is_transitive_in X
proof
let R be Relation; ::_thesis: for X being set st R is_transitive_in X holds
R ~ is_transitive_in X
let X be set ; ::_thesis: ( R is_transitive_in X implies R ~ is_transitive_in X )
assume A1: for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds
[x,z] in R ; :: according to RELAT_2:def_8 ::_thesis: R ~ is_transitive_in X
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in X or not b1 in X or not b2 in X or not [x,b1] in R ~ or not [b1,b2] in R ~ or [x,b2] in R ~ )
let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in R ~ or not [y,z] in R ~ or [x,z] in R ~ )
assume that
A2: x in X and
A3: y in X and
A4: z in X and
A5: [x,y] in R ~ and
A6: [y,z] in R ~ ; ::_thesis: [x,z] in R ~
A7: [z,y] in R by A6, RELAT_1:def_7;
 [y,x] in R by A5, RELAT_1:def_7;
then  [z,x] in R by A1, A2, A3, A4, A7;
hence  [x,z] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;

Lm13:  for R being Relation
for X being set st R is_antisymmetric_in X holds
R ~ is_antisymmetric_in X
proof
let R be Relation; ::_thesis: for X being set st R is_antisymmetric_in X holds
R ~ is_antisymmetric_in X
let X be set ; ::_thesis: ( R is_antisymmetric_in X implies R ~ is_antisymmetric_in X )
assume A1: for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y ; :: according to RELAT_2:def_4 ::_thesis: R ~ is_antisymmetric_in X
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or not [x,b1] in R ~ or not [b1,x] in R ~ or x = b1 )
let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in R ~ or not [y,x] in R ~ or x = y )
assume that
A2: x in X and
A3: y in X and
A4: [x,y] in R ~ and
A5: [y,x] in R ~ ; ::_thesis: x = y
A6: [y,x] in R by A4, RELAT_1:def_7;
 [x,y] in R by A5, RELAT_1:def_7;
hence  x = y by A1, A2, A3, A6; ::_thesis: verum
end;

Lm14:  for R being Relation
for X being set st R is_connected_in X holds
R ~ is_connected_in X
proof
let R be Relation; ::_thesis: for X being set st R is_connected_in X holds
R ~ is_connected_in X
let X be set ; ::_thesis: ( R is_connected_in X implies R ~ is_connected_in X )
assume A1: for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds
[y,x] in R ; :: according to RELAT_2:def_6 ::_thesis: R ~ is_connected_in X
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or x = b1 or [x,b1] in R ~ or [b1,x] in R ~ )
let y be set ; ::_thesis: ( not x in X or not y in X or x = y or [x,y] in R ~ or [y,x] in R ~ )
assume that
A2: x in X and
A3: y in X and
A4: x <> y ; ::_thesis: ( [x,y] in R ~ or [y,x] in R ~ )
 ( [x,y] in R or [y,x] in R ) by A1, A2, A3, A4;
hence  ( [x,y] in R ~ or [y,x] in R ~ ) by RELAT_1:def_7; ::_thesis: verum
end;

theorem :: ORDERS_1:40
for R being Relation
for X being set st R quasi_orders X holds
R ~ quasi_orders X
proof
let R be Relation; ::_thesis: for X being set st R quasi_orders X holds
R ~ quasi_orders X
let X be set ; ::_thesis: ( R quasi_orders X implies R ~ quasi_orders X )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X ; :: according to ORDERS_1:def_6 ::_thesis: R ~ quasi_orders X
thus  ( R ~ is_reflexive_in X & R ~ is_transitive_in X ) by A1, A2, Lm11, Lm12; :: according to ORDERS_1:def_6 ::_thesis: verum
end;

theorem Th41: :: ORDERS_1:41
for R being Relation
for X being set st R partially_orders X holds
R ~ partially_orders X
proof
let R be Relation; ::_thesis: for X being set st R partially_orders X holds
R ~ partially_orders X
let X be set ; ::_thesis: ( R partially_orders X implies R ~ partially_orders X )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X and
A3: R is_antisymmetric_in X ; :: according to ORDERS_1:def_7 ::_thesis: R ~ partially_orders X
thus  ( R ~ is_reflexive_in X & R ~ is_transitive_in X & R ~ is_antisymmetric_in X ) by A1, A2, A3, Lm11, Lm12, Lm13; :: according to ORDERS_1:def_7 ::_thesis: verum
end;

theorem :: ORDERS_1:42
for R being Relation
for X being set st R linearly_orders X holds
R ~ linearly_orders X
proof
let R be Relation; ::_thesis: for X being set st R linearly_orders X holds
R ~ linearly_orders X
let X be set ; ::_thesis: ( R linearly_orders X implies R ~ linearly_orders X )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X and
A3: R is_antisymmetric_in X and
A4: R is_connected_in X ; :: according to ORDERS_1:def_8 ::_thesis: R ~ linearly_orders X
thus  ( R ~ is_reflexive_in X & R ~ is_transitive_in X & R ~ is_antisymmetric_in X & R ~ is_connected_in X ) by A1, A2, A3, A4, Lm11, Lm12, Lm13, Lm14; :: according to ORDERS_1:def_8 ::_thesis: verum
end;

theorem :: ORDERS_1:43
for X being set
for O being Order of X holds O quasi_orders X
proof
let X be set ; ::_thesis: for O being Order of X holds O quasi_orders X
let O be Order of X; ::_thesis: O quasi_orders X
A1: field O = X by Lm2;
then A2: O is_transitive_in X by RELAT_2:def_16;
 O is_reflexive_in X by A1, RELAT_2:def_9;
hence  O quasi_orders X by A2, Def6; ::_thesis: verum
end;

theorem :: ORDERS_1:44
for X being set
for O being Order of X holds O partially_orders X
proof
let X be set ; ::_thesis: for O being Order of X holds O partially_orders X
let O be Order of X; ::_thesis: O partially_orders X
A1: field O = X by Lm2;
then A2: O is_antisymmetric_in X by RELAT_2:def_12;
A3: O is_transitive_in X by A1, RELAT_2:def_16;
 O is_reflexive_in X by A1, RELAT_2:def_9;
hence  O partially_orders X by A2, A3, Def7; ::_thesis: verum
end;

theorem Th45: :: ORDERS_1:45
for R being Relation
for X being set st R partially_orders X holds
R |_2 X is Order of X
proof
let R be Relation; ::_thesis: for X being set st R partially_orders X holds
R |_2 X is Order of X
let X be set ; ::_thesis: ( R partially_orders X implies R |_2 X is Order of X )
set S = R |_2 X;
A1: field (R |_2 X) c= X by WELLORD1:13;
 rng (R |_2 X) c= field (R |_2 X) by XBOOLE_1:7;
then A2: rng (R |_2 X) c= X by A1, XBOOLE_1:1;
 dom (R |_2 X) c= field (R |_2 X) by XBOOLE_1:7;
then  dom (R |_2 X) c= X by A1, XBOOLE_1:1;
then reconsider S = R |_2 X as Relation of X by A2, RELSET_1:4;
assume A3: R partially_orders X ; ::_thesis: R |_2 X is Order of X
A4: R |_2 X is_antisymmetric_in X
proof
A5: R is_antisymmetric_in X by A3, Def7;
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or not [x,b1] in R |_2 X or not [b1,x] in R |_2 X or x = b1 )
let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y )
assume that
A6: x in X and
A7: y in X and
A8: [x,y] in R |_2 X and
A9: [y,x] in R |_2 X ; ::_thesis: x = y
A10: [y,x] in R by A9, XBOOLE_0:def_4;
 [x,y] in R by A8, XBOOLE_0:def_4;
hence  x = y by A6, A7, A10, A5, RELAT_2:def_4; ::_thesis: verum
end;
A11: R |_2 X is_transitive_in X
proof
A12: R is_transitive_in X by A3, Def7;
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in X or not b1 in X or not b2 in X or not [x,b1] in R |_2 X or not [b1,b2] in R |_2 X or [x,b2] in R |_2 X )
let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X )
assume that
A13: x in X and
A14: y in X and
A15: z in X and
A16: [x,y] in R |_2 X and
A17: [y,z] in R |_2 X ; ::_thesis: [x,z] in R |_2 X
A18: [x,z] in [:X,X:] by A13, A15, ZFMISC_1:87;
A19: [y,z] in R by A17, XBOOLE_0:def_4;
 [x,y] in R by A16, XBOOLE_0:def_4;
then  [x,z] in R by A13, A14, A15, A19, A12, RELAT_2:def_8;
hence  [x,z] in R |_2 X by A18, XBOOLE_0:def_4; ::_thesis: verum
end;
A20: R is_reflexive_in X by A3, Def7;
A21: R |_2 X is_reflexive_in X
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in R |_2 X )
assume A22: x in X ; ::_thesis: [x,x] in R |_2 X
then A23: [x,x] in [:X,X:] by ZFMISC_1:87;
 [x,x] in R by A20, A22, RELAT_2:def_1;
hence  [x,x] in R |_2 X by A23, XBOOLE_0:def_4; ::_thesis: verum
end;
then A24: field S = X by Th13;
 dom S = X by A21, Th13;
hence  R |_2 X is Order of X by A21, A24, A4, A11, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16; ::_thesis: verum
end;

theorem :: ORDERS_1:46
for R being Relation
for X being set st R linearly_orders X holds
R |_2 X is Order of X by Th29, Th45;

theorem :: ORDERS_1:47
for R being Relation
for X being set st R well_orders X holds
R |_2 X is Order of X by Th28, Th45;

theorem :: ORDERS_1:48
for X being set holds
( id X quasi_orders X & id X partially_orders X )
proof
let X be set ; ::_thesis: ( id X quasi_orders X & id X partially_orders X )
field (id X) = X \/ (rng (id X))
.= X \/ X
.= X ;
hence  ( id X quasi_orders X & id X partially_orders X ) by Th31, Th34; ::_thesis: verum
end;

definition
let R be Relation;
let X be set ;
predX has_upper_Zorn_property_wrt R means :Def9: :: ORDERS_1:def 9
 for Y being set st Y c= X & R |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) );
predX has_lower_Zorn_property_wrt R means :: ORDERS_1:def 10
 for Y being set st Y c= X & R |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ) );
end;

:: deftheorem Def9 defines has_upper_Zorn_property_wrt ORDERS_1:def_9_:_
 for R being Relation
for X being set holds
( X has_upper_Zorn_property_wrt R iff for Y being set st Y c= X & R |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) ) );

:: deftheorem  defines has_lower_Zorn_property_wrt ORDERS_1:def_10_:_
 for R being Relation
for X being set holds
( X has_lower_Zorn_property_wrt R iff for Y being set st Y c= X & R |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ) ) );

Lm15:  for R being Relation
for X being set holds (R |_2 X) ~ = (R ~) |_2 X
proof
let R be Relation; ::_thesis: for X being set holds (R |_2 X) ~ = (R ~) |_2 X
let X be set ; ::_thesis: (R |_2 X) ~ = (R ~) |_2 X
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_(R_~)_|_2_X_implies_[y,x]_in_R_|_2_X_)_&_(_[y,x]_in_R_|_2_X_implies_[x,y]_in_(R_~)_|_2_X_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in (R ~) |_2 X implies [y,x] in R |_2 X ) & ( [y,x] in R |_2 X implies [x,y] in (R ~) |_2 X ) )
thus  ( [x,y] in (R ~) |_2 X implies [y,x] in R |_2 X ) ::_thesis: ( [y,x] in R |_2 X implies [x,y] in (R ~) |_2 X )
proof
assume A1: [x,y] in (R ~) |_2 X ; ::_thesis: [y,x] in R |_2 X
then  [x,y] in [:X,X:] by XBOOLE_0:def_4;
then A2: [y,x] in [:X,X:] by ZFMISC_1:88;
 [x,y] in R ~ by A1, XBOOLE_0:def_4;
then  [y,x] in R by RELAT_1:def_7;
hence  [y,x] in R |_2 X by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A3: [y,x] in R |_2 X ; ::_thesis: [x,y] in (R ~) |_2 X
then  [y,x] in [:X,X:] by XBOOLE_0:def_4;
then A4: [x,y] in [:X,X:] by ZFMISC_1:88;
 [y,x] in R by A3, XBOOLE_0:def_4;
then  [x,y] in R ~ by RELAT_1:def_7;
hence  [x,y] in (R ~) |_2 X by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  (R |_2 X) ~ = (R ~) |_2 X by RELAT_1:def_7; ::_thesis: verum
end;

Lm16: now__::_thesis:_for_R_being_Relation_holds_R_|_2_{}_=_{}
let R be Relation; ::_thesis: R |_2 {} = {}
thus R |_2 {} = ({} |` R) | {} by WELLORD1:10
.= {} ; ::_thesis: verum
end;

theorem Th49: :: ORDERS_1:49
for R being Relation
for X being set st X has_upper_Zorn_property_wrt R holds
X <> {}
proof
let R be Relation; ::_thesis: for X being set st X has_upper_Zorn_property_wrt R holds
X <> {}
let X be set ; ::_thesis: ( X has_upper_Zorn_property_wrt R implies X <> {} )
assume A1: for Y being set st Y c= X & R |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) ) ; :: according to ORDERS_1:def_9 ::_thesis: X <> {}
 R |_2 {} is being_linear-order by Lm16;
then  ex x being set st
( x in X & ( for y being set st y in {} holds
[y,x] in R ) ) by A1, XBOOLE_1:2;
hence  X <> {} ; ::_thesis: verum
end;

theorem :: ORDERS_1:50
for R being Relation
for X being set st X has_lower_Zorn_property_wrt R holds
X <> {}
proof
let R be Relation; ::_thesis: for X being set st X has_lower_Zorn_property_wrt R holds
X <> {}
let X be set ; ::_thesis: ( X has_lower_Zorn_property_wrt R implies X <> {} )
assume A1: for Y being set st Y c= X & R |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ) ) ; :: according to ORDERS_1:def_10 ::_thesis: X <> {}
 R |_2 {} is being_linear-order by Lm16;
then  ex x being set st
( x in X & ( for y being set st y in {} holds
[x,y] in R ) ) by A1, XBOOLE_1:2;
hence  X <> {} ; ::_thesis: verum
end;

theorem Th51: :: ORDERS_1:51
for R being Relation
for X being set holds
( X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R ~ )
proof
let R be Relation; ::_thesis: for X being set holds
( X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R ~ )
let X be set ; ::_thesis: ( X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R ~ )
thus  ( X has_upper_Zorn_property_wrt R implies X has_lower_Zorn_property_wrt R ~ ) ::_thesis: ( X has_lower_Zorn_property_wrt R ~ implies X has_upper_Zorn_property_wrt R )
proof
assume A1: for Y being set st Y c= X & R |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) ) ; :: according to ORDERS_1:def_9 ::_thesis: X has_lower_Zorn_property_wrt R ~
let Y be set ; :: according to ORDERS_1:def_10 ::_thesis: ( Y c= X & (R ~) |_2 Y is being_linear-order implies ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) ) )
A2: ((R |_2 Y) ~) ~ = R |_2 Y ;
assume that
A3: Y c= X and
A4: (R ~) |_2 Y is being_linear-order ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) )
 (R ~) |_2 Y = (R |_2 Y) ~ by Lm15;
then consider x being set  such that
A5: x in X and
A6: for y being set st y in Y holds
[y,x] in R by A1, A2, A3, A4, Th18;
take  x ; ::_thesis: ( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) )
thus  x in X by A5; ::_thesis: for y being set st y in Y holds
[x,y] in R ~
let y be set ; ::_thesis: ( y in Y implies [x,y] in R ~ )
assume  y in Y ; ::_thesis: [x,y] in R ~
then  [y,x] in R by A6;
hence  [x,y] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;
assume A7: for Y being set st Y c= X & (R ~) |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) ) ; :: according to ORDERS_1:def_10 ::_thesis: X has_upper_Zorn_property_wrt R
let Y be set ; :: according to ORDERS_1:def_9 ::_thesis: ( Y c= X & R |_2 Y is being_linear-order implies ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) ) )
assume that
A8: Y c= X and
A9: R |_2 Y is being_linear-order ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) )
 (R ~) |_2 Y = (R |_2 Y) ~ by Lm15;
then consider x being set  such that
A10: x in X and
A11: for y being set st y in Y holds
[x,y] in R ~ by A7, A8, A9, Th18;
take  x ; ::_thesis: ( x in X & ( for y being set st y in Y holds
[y,x] in R ) )
thus  x in X by A10; ::_thesis: for y being set st y in Y holds
[y,x] in R
let y be set ; ::_thesis: ( y in Y implies [y,x] in R )
assume  y in Y ; ::_thesis: [y,x] in R
then  [x,y] in R ~ by A11;
hence  [y,x] in R by RELAT_1:def_7; ::_thesis: verum
end;

theorem :: ORDERS_1:52
for R being Relation
for X being set holds
( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R )
proof
let R be Relation; ::_thesis: for X being set holds
( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R )
let X be set ; ::_thesis: ( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R )
 (R ~) ~ = R ;
hence  ( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R ) by Th51; ::_thesis: verum
end;

definition
let R be Relation;
let x be set ;
predx is_maximal_in R means :Def11: :: ORDERS_1:def 11
( x in field R & ( for y being set holds
( not y in field R or not y <> x or not [x,y] in R ) ) );
predx is_minimal_in R means :Def12: :: ORDERS_1:def 12
( x in field R & ( for y being set holds
( not y in field R or not y <> x or not [y,x] in R ) ) );
predx is_superior_of R means :Def13: :: ORDERS_1:def 13
( x in field R & ( for y being set st y in field R & y <> x holds
[y,x] in R ) );
predx is_inferior_of R means :Def14: :: ORDERS_1:def 14
( x in field R & ( for y being set st y in field R & y <> x holds
[x,y] in R ) );
end;

:: deftheorem Def11 defines is_maximal_in ORDERS_1:def_11_:_
 for R being Relation
for x being set holds
( x is_maximal_in R iff ( x in field R & ( for y being set holds
( not y in field R or not y <> x or not [x,y] in R ) ) ) );

:: deftheorem Def12 defines is_minimal_in ORDERS_1:def_12_:_
 for R being Relation
for x being set holds
( x is_minimal_in R iff ( x in field R & ( for y being set holds
( not y in field R or not y <> x or not [y,x] in R ) ) ) );

:: deftheorem Def13 defines is_superior_of ORDERS_1:def_13_:_
 for R being Relation
for x being set holds
( x is_superior_of R iff ( x in field R & ( for y being set st y in field R & y <> x holds
[y,x] in R ) ) );

:: deftheorem Def14 defines is_inferior_of ORDERS_1:def_14_:_
 for R being Relation
for x being set holds
( x is_inferior_of R iff ( x in field R & ( for y being set st y in field R & y <> x holds
[x,y] in R ) ) );

theorem :: ORDERS_1:53
for R being Relation
for x being set st x is_inferior_of R & R is antisymmetric holds
x is_minimal_in R
proof
let R be Relation; ::_thesis: for x being set st x is_inferior_of R & R is antisymmetric holds
x is_minimal_in R
let x be set ; ::_thesis: ( x is_inferior_of R & R is antisymmetric implies x is_minimal_in R )
assume that
A1: x is_inferior_of R and
A2: R is antisymmetric ; ::_thesis: x is_minimal_in R
A3: R is_antisymmetric_in field R by A2, RELAT_2:def_12;
thus A4: x in field R by A1, Def14; :: according to ORDERS_1:def_12 ::_thesis: for y being set holds
( not y in field R or not y <> x or not [y,x] in R )
let y be set ; ::_thesis: ( not y in field R or not y <> x or not [y,x] in R )
assume that
A5: y in field R and
A6: y <> x and
A7: [y,x] in R ; ::_thesis: contradiction
 [x,y] in R by A1, A5, A6, Def14;
hence  contradiction by A4, A5, A6, A7, A3, RELAT_2:def_4; ::_thesis: verum
end;

theorem :: ORDERS_1:54
for R being Relation
for x being set st x is_superior_of R & R is antisymmetric holds
x is_maximal_in R
proof
let R be Relation; ::_thesis: for x being set st x is_superior_of R & R is antisymmetric holds
x is_maximal_in R
let x be set ; ::_thesis: ( x is_superior_of R & R is antisymmetric implies x is_maximal_in R )
assume that
A1: x is_superior_of R and
A2: R is antisymmetric ; ::_thesis: x is_maximal_in R
A3: R is_antisymmetric_in field R by A2, RELAT_2:def_12;
thus A4: x in field R by A1, Def13; :: according to ORDERS_1:def_11 ::_thesis: for y being set holds
( not y in field R or not y <> x or not [x,y] in R )
let y be set ; ::_thesis: ( not y in field R or not y <> x or not [x,y] in R )
assume that
A5: y in field R and
A6: y <> x and
A7: [x,y] in R ; ::_thesis: contradiction
 [y,x] in R by A1, A5, A6, Def13;
hence  contradiction by A4, A5, A6, A7, A3, RELAT_2:def_4; ::_thesis: verum
end;

theorem :: ORDERS_1:55
for R being Relation
for x being set st x is_minimal_in R & R is connected holds
x is_inferior_of R
proof
let R be Relation; ::_thesis: for x being set st x is_minimal_in R & R is connected holds
x is_inferior_of R
let x be set ; ::_thesis: ( x is_minimal_in R & R is connected implies x is_inferior_of R )
assume that
A1: x is_minimal_in R and
A2: R is connected ; ::_thesis: x is_inferior_of R
thus A3: x in field R by A1, Def12; :: according to ORDERS_1:def_14 ::_thesis: for y being set st y in field R & y <> x holds
[x,y] in R
let y be set ; ::_thesis: ( y in field R & y <> x implies [x,y] in R )
assume that
A4: y in field R and
A5: y <> x ; ::_thesis: [x,y] in R
 R is_connected_in field R by A2, RELAT_2:def_14;
then  ( [x,y] in R or [y,x] in R ) by A3, A4, A5, RELAT_2:def_6;
hence  [x,y] in R by A1, A4, Def12; ::_thesis: verum
end;

theorem :: ORDERS_1:56
for R being Relation
for x being set st x is_maximal_in R & R is connected holds
x is_superior_of R
proof
let R be Relation; ::_thesis: for x being set st x is_maximal_in R & R is connected holds
x is_superior_of R
let x be set ; ::_thesis: ( x is_maximal_in R & R is connected implies x is_superior_of R )
assume that
A1: x is_maximal_in R and
A2: R is connected ; ::_thesis: x is_superior_of R
thus A3: x in field R by A1, Def11; :: according to ORDERS_1:def_13 ::_thesis: for y being set st y in field R & y <> x holds
[y,x] in R
let y be set ; ::_thesis: ( y in field R & y <> x implies [y,x] in R )
assume that
A4: y in field R and
A5: y <> x ; ::_thesis: [y,x] in R
 R is_connected_in field R by A2, RELAT_2:def_14;
then  ( [x,y] in R or [y,x] in R ) by A3, A4, A5, RELAT_2:def_6;
hence  [y,x] in R by A1, A4, Def11; ::_thesis: verum
end;

theorem :: ORDERS_1:57
for R being Relation
for x, X being set st x in X & x is_superior_of R & X c= field R & R is reflexive holds
X has_upper_Zorn_property_wrt R
proof
let R be Relation; ::_thesis: for x, X being set st x in X & x is_superior_of R & X c= field R & R is reflexive holds
X has_upper_Zorn_property_wrt R
let x, X be set ; ::_thesis: ( x in X & x is_superior_of R & X c= field R & R is reflexive implies X has_upper_Zorn_property_wrt R )
assume that
A1: x in X and
A2: x is_superior_of R and
A3: X c= field R and
A4: R is_reflexive_in field R ; :: according to RELAT_2:def_9 ::_thesis: X has_upper_Zorn_property_wrt R
let Y be set ; :: according to ORDERS_1:def_9 ::_thesis: ( Y c= X & R |_2 Y is being_linear-order implies ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) ) )
assume that
A5: Y c= X and
 R |_2 Y is being_linear-order ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) )
take  x ; ::_thesis: ( x in X & ( for y being set st y in Y holds
[y,x] in R ) )
thus  x in X by A1; ::_thesis: for y being set st y in Y holds
[y,x] in R
let y be set ; ::_thesis: ( y in Y implies [y,x] in R )
assume  y in Y ; ::_thesis: [y,x] in R
then A6: y in X by A5;
 ( y = x or y <> x ) ;
hence  [y,x] in R by A2, A3, A4, A6, Def13, RELAT_2:def_1; ::_thesis: verum
end;

theorem :: ORDERS_1:58
for R being Relation
for x, X being set st x in X & x is_inferior_of R & X c= field R & R is reflexive holds
X has_lower_Zorn_property_wrt R
proof
let R be Relation; ::_thesis: for x, X being set st x in X & x is_inferior_of R & X c= field R & R is reflexive holds
X has_lower_Zorn_property_wrt R
let x, X be set ; ::_thesis: ( x in X & x is_inferior_of R & X c= field R & R is reflexive implies X has_lower_Zorn_property_wrt R )
assume that
A1: x in X and
A2: x is_inferior_of R and
A3: X c= field R and
A4: R is_reflexive_in field R ; :: according to RELAT_2:def_9 ::_thesis: X has_lower_Zorn_property_wrt R
let Y be set ; :: according to ORDERS_1:def_10 ::_thesis: ( Y c= X & R |_2 Y is being_linear-order implies ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ) ) )
assume that
A5: Y c= X and
 R |_2 Y is being_linear-order ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ) )
take  x ; ::_thesis: ( x in X & ( for y being set st y in Y holds
[x,y] in R ) )
thus  x in X by A1; ::_thesis: for y being set st y in Y holds
[x,y] in R
let y be set ; ::_thesis: ( y in Y implies [x,y] in R )
assume  y in Y ; ::_thesis: [x,y] in R
then A6: y in X by A5;
 ( y = x or y <> x ) ;
hence  [x,y] in R by A2, A3, A4, A6, Def14, RELAT_2:def_1; ::_thesis: verum
end;

theorem Th59: :: ORDERS_1:59
for R being Relation
for x being set holds
( x is_minimal_in R iff x is_maximal_in R ~ )
proof
let R be Relation; ::_thesis: for x being set holds
( x is_minimal_in R iff x is_maximal_in R ~ )
let x be set ; ::_thesis: ( x is_minimal_in R iff x is_maximal_in R ~ )
A1: field R = field (R ~) by RELAT_1:21;
thus  ( x is_minimal_in R implies x is_maximal_in R ~ ) ::_thesis: ( x is_maximal_in R ~ implies x is_minimal_in R )
proof
assume that
A2: x in field R and
A3: for y being set holds
( not y in field R or not y <> x or not [y,x] in R ) ; :: according to ORDERS_1:def_12 ::_thesis: x is_maximal_in R ~
thus  x in field (R ~) by A2, RELAT_1:21; :: according to ORDERS_1:def_11 ::_thesis: for y being set holds
( not y in field (R ~) or not y <> x or not [x,y] in R ~ )
let y be set ; ::_thesis: ( not y in field (R ~) or not y <> x or not [x,y] in R ~ )
assume that
A4: y in field (R ~) and
A5: y <> x ; ::_thesis: not [x,y] in R ~
 not [y,x] in R by A1, A3, A4, A5;
hence  not [x,y] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;
assume that
A6: x in field (R ~) and
A7: for y being set holds
( not y in field (R ~) or not y <> x or not [x,y] in R ~ ) ; :: according to ORDERS_1:def_11 ::_thesis: x is_minimal_in R
thus  x in field R by A6, RELAT_1:21; :: according to ORDERS_1:def_12 ::_thesis: for y being set holds
( not y in field R or not y <> x or not [y,x] in R )
let y be set ; ::_thesis: ( not y in field R or not y <> x or not [y,x] in R )
assume that
A8: y in field R and
A9: y <> x ; ::_thesis: not [y,x] in R
 not [x,y] in R ~ by A1, A7, A8, A9;
hence  not [y,x] in R by RELAT_1:def_7; ::_thesis: verum
end;

theorem :: ORDERS_1:60
for R being Relation
for x being set holds
( x is_minimal_in R ~ iff x is_maximal_in R )
proof
let R be Relation; ::_thesis: for x being set holds
( x is_minimal_in R ~ iff x is_maximal_in R )
let x be set ; ::_thesis: ( x is_minimal_in R ~ iff x is_maximal_in R )
A1: field R = field (R ~) by RELAT_1:21;
thus  ( x is_minimal_in R ~ implies x is_maximal_in R ) ::_thesis: ( x is_maximal_in R implies x is_minimal_in R ~ )
proof
assume that
A2: x in field (R ~) and
A3: for y being set holds
( not y in field (R ~) or not y <> x or not [y,x] in R ~ ) ; :: according to ORDERS_1:def_12 ::_thesis: x is_maximal_in R
thus  x in field R by A2, RELAT_1:21; :: according to ORDERS_1:def_11 ::_thesis: for y being set holds
( not y in field R or not y <> x or not [x,y] in R )
let y be set ; ::_thesis: ( not y in field R or not y <> x or not [x,y] in R )
assume that
A4: y in field R and
A5: y <> x ; ::_thesis: not [x,y] in R
 not [y,x] in R ~ by A1, A3, A4, A5;
hence  not [x,y] in R by RELAT_1:def_7; ::_thesis: verum
end;
assume that
A6: x in field R and
A7: for y being set holds
( not y in field R or not y <> x or not [x,y] in R ) ; :: according to ORDERS_1:def_11 ::_thesis: x is_minimal_in R ~
thus  x in field (R ~) by A6, RELAT_1:21; :: according to ORDERS_1:def_12 ::_thesis: for y being set holds
( not y in field (R ~) or not y <> x or not [y,x] in R ~ )
let y be set ; ::_thesis: ( not y in field (R ~) or not y <> x or not [y,x] in R ~ )
assume that
A8: y in field (R ~) and
A9: y <> x ; ::_thesis: not [y,x] in R ~
 not [x,y] in R by A1, A7, A8, A9;
hence  not [y,x] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;

theorem :: ORDERS_1:61
for R being Relation
for x being set holds
( x is_inferior_of R iff x is_superior_of R ~ )
proof
let R be Relation; ::_thesis: for x being set holds
( x is_inferior_of R iff x is_superior_of R ~ )
let x be set ; ::_thesis: ( x is_inferior_of R iff x is_superior_of R ~ )
A1: field R = field (R ~) by RELAT_1:21;
thus  ( x is_inferior_of R implies x is_superior_of R ~ ) ::_thesis: ( x is_superior_of R ~ implies x is_inferior_of R )
proof
assume that
A2: x in field R and
A3: for y being set st y in field R & y <> x holds
[x,y] in R ; :: according to ORDERS_1:def_14 ::_thesis: x is_superior_of R ~
thus  x in field (R ~) by A2, RELAT_1:21; :: according to ORDERS_1:def_13 ::_thesis: for y being set st y in field (R ~) & y <> x holds
[y,x] in R ~
let y be set ; ::_thesis: ( y in field (R ~) & y <> x implies [y,x] in R ~ )
assume that
A4: y in field (R ~) and
A5: y <> x ; ::_thesis: [y,x] in R ~
 [x,y] in R by A1, A3, A4, A5;
hence  [y,x] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;
assume that
A6: x in field (R ~) and
A7: for y being set st y in field (R ~) & y <> x holds
[y,x] in R ~ ; :: according to ORDERS_1:def_13 ::_thesis: x is_inferior_of R
thus  x in field R by A6, RELAT_1:21; :: according to ORDERS_1:def_14 ::_thesis: for y being set st y in field R & y <> x holds
[x,y] in R
let y be set ; ::_thesis: ( y in field R & y <> x implies [x,y] in R )
assume that
A8: y in field R and
A9: y <> x ; ::_thesis: [x,y] in R
 [y,x] in R ~ by A1, A7, A8, A9;
hence  [x,y] in R by RELAT_1:def_7; ::_thesis: verum
end;

theorem :: ORDERS_1:62
for R being Relation
for x being set holds
( x is_inferior_of R ~ iff x is_superior_of R )
proof
let R be Relation; ::_thesis: for x being set holds
( x is_inferior_of R ~ iff x is_superior_of R )
let x be set ; ::_thesis: ( x is_inferior_of R ~ iff x is_superior_of R )
A1: field R = field (R ~) by RELAT_1:21;
thus  ( x is_inferior_of R ~ implies x is_superior_of R ) ::_thesis: ( x is_superior_of R implies x is_inferior_of R ~ )
proof
assume that
A2: x in field (R ~) and
A3: for y being set st y in field (R ~) & y <> x holds
[x,y] in R ~ ; :: according to ORDERS_1:def_14 ::_thesis: x is_superior_of R
thus  x in field R by A2, RELAT_1:21; :: according to ORDERS_1:def_13 ::_thesis: for y being set st y in field R & y <> x holds
[y,x] in R
let y be set ; ::_thesis: ( y in field R & y <> x implies [y,x] in R )
assume that
A4: y in field R and
A5: y <> x ; ::_thesis: [y,x] in R
 [x,y] in R ~ by A1, A3, A4, A5;
hence  [y,x] in R by RELAT_1:def_7; ::_thesis: verum
end;
assume that
A6: x in field R and
A7: for y being set st y in field R & y <> x holds
[y,x] in R ; :: according to ORDERS_1:def_13 ::_thesis: x is_inferior_of R ~
thus  x in field (R ~) by A6, RELAT_1:21; :: according to ORDERS_1:def_14 ::_thesis: for y being set st y in field (R ~) & y <> x holds
[x,y] in R ~
let y be set ; ::_thesis: ( y in field (R ~) & y <> x implies [x,y] in R ~ )
assume that
A8: y in field (R ~) and
A9: y <> x ; ::_thesis: [x,y] in R ~
 [y,x] in R by A1, A7, A8, A9;
hence  [x,y] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;

Lm17:  for R being Relation
for X, Y being set st R well_orders X & Y c= X holds
R well_orders Y
proof
let R be Relation; ::_thesis: for X, Y being set st R well_orders X & Y c= X holds
R well_orders Y
let X, Y be set ; ::_thesis: ( R well_orders X & Y c= X implies R well_orders Y )
assume that
A1: R well_orders X and
A2: Y c= X ; ::_thesis: R well_orders Y
A3: R is_transitive_in X by A1, WELLORD1:def_5;
A4: R is_connected_in X by A1, WELLORD1:def_5;
A5: R is_antisymmetric_in X by A1, WELLORD1:def_5;
A6: R is_well_founded_in X by A1, WELLORD1:def_5;
 R is_reflexive_in X by A1, WELLORD1:def_5;
hence  ( R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y & R is_connected_in Y ) by A2, A3, A5, A4, Lm10, Th8, Th9, Th10; :: according to WELLORD1:def_5 ::_thesis: R is_well_founded_in Y
let Z be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Z c= Y or Z = {} or ex b1 being set st
( b1 in Z & R -Seg b1 misses Z ) )
assume that
A7: Z c= Y and
A8: Z <> {} ; ::_thesis: ex b1 being set st
( b1 in Z & R -Seg b1 misses Z )
 Z c= X by A2, A7, XBOOLE_1:1;
hence  ex b1 being set st
( b1 in Z & R -Seg b1 misses Z ) by A8, A6, WELLORD1:def_3; ::_thesis: verum
end;


theorem Th63: :: ORDERS_1:63
for R being Relation
for X being set st R partially_orders X & field R = X & X has_upper_Zorn_property_wrt R holds
ex x being set st x is_maximal_in R
proof
let R be Relation; ::_thesis: for X being set st R partially_orders X & field R = X & X has_upper_Zorn_property_wrt R holds
ex x being set st x is_maximal_in R
let FIELD be set ; ::_thesis: ( R partially_orders FIELD & field R = FIELD & FIELD has_upper_Zorn_property_wrt R implies ex x being set st x is_maximal_in R )
assume that
A1: R is_reflexive_in FIELD and
A2: R is_transitive_in FIELD and
A3: R is_antisymmetric_in FIELD and
A4: field R = FIELD and
A5: FIELD has_upper_Zorn_property_wrt R ; :: according to ORDERS_1:def_7 ::_thesis: ex x being set st x is_maximal_in R
reconsider XD = FIELD as non empty set by A5, Th49;
consider D being non empty set  such that
A6: D = XD ;
A7: D in bool D by ZFMISC_1:def_1;
 not D in {{}} by TARSKI:def_1;
then reconsider M = (bool D) \ {{}} as non empty set by A7, XBOOLE_0:def_5;
set f = the Choice_Function of M;
defpred S1[ set , set ] means ( ( $1 <> {} & $2 = the Choice_Function of M . $1 ) or ( $1 = {} & $2 = D ) );
A8: for x being set st x in bool D holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in bool D implies ex y being set st S1[x,y] )
assume  x in bool D ; ::_thesis: ex y being set st S1[x,y]
 ( x = {} implies ex y being set st S1[x,y] ) ;
hence  ex y being set st S1[x,y] ; ::_thesis: verum
end;
A9: for x, y, z being set st x in bool D & S1[x,y] & S1[x,z] holds
y = z ;
consider g being Function such that
A10: ( dom g = bool D & ( for x being set st x in bool D holds
S1[x,g . x] ) ) from FUNCT_1:sch_2(A9, A8);
defpred S2[ Ordinal, set ] means  ex L being T-Sequence st
( $2 = g .  {  d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R )  }  & dom L = $1 & ( for A being Ordinal
for L1 being T-Sequence st A in $1 & L1 = L | A holds
L . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ) );
A11: for x, y being set
for A being Ordinal st S2[A,x] & S2[A,y] holds
x = y
proof
let x, y be set ; ::_thesis: for A being Ordinal st S2[A,x] & S2[A,y] holds
x = y
let A be Ordinal; ::_thesis: ( S2[A,x] & S2[A,y] implies x = y )
given L1 being T-Sequence such that A12: x = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  and
A13: ( dom L1 = A & ( for C being Ordinal
for L being T-Sequence st C in A & L = L1 | C holds
L1 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) ) ; ::_thesis: ( not S2[A,y] or x = y )
A14: L1 = L1 | A by A13, RELAT_1:68;
given L2 being T-Sequence such that A15: y = g .  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  and
A16: ( dom L2 = A & ( for C being Ordinal
for L being T-Sequence st C in A & L = L2 | C holds
L2 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) ) ; ::_thesis: x = y
defpred S3[ Ordinal] means ( $1 c= A implies L1 | $1 = L2 | $1 );
A17: for A1 being Ordinal st ( for A2 being Ordinal st A2 in A1 holds
S3[A2] ) holds
S3[A1]
proof
let A1 be Ordinal; ::_thesis: ( ( for A2 being Ordinal st A2 in A1 holds
S3[A2] ) implies S3[A1] )
assume that
A18: for A2 being Ordinal st A2 in A1 & A2 c= A holds
L1 | A2 = L2 | A2 and
A19: A1 c= A ; ::_thesis: L1 | A1 = L2 | A1
A20: dom (L2 | A1) = A1 by A16, A19, RELAT_1:62;
A21: now__::_thesis:_for_x_being_set_st_x_in_A1_holds_
(L1_|_A1)_._x_=_(L2_|_A1)_._x
let x be set ; ::_thesis: ( x in A1 implies (L1 | A1) . x = (L2 | A1) . x )
assume A22: x in A1 ; ::_thesis: (L1 | A1) . x = (L2 | A1) . x
then reconsider A3 = x as Ordinal ;
A23: L1 . x = (L1 | A1) . x by A22, FUNCT_1:49;
 A3 c= A by A19, A22, ORDINAL1:def_2;
then A24: L1 | A3 = L2 | A3 by A18, A22;
A25: L2 . A3 = g .  {  d2 where d2 is Element of D : for x being set st x in rng (L2 | A3) holds
( x <> d2 & [x,d2] in R )  }  by A16, A19, A22;
 L1 . A3 = g .  {  d1 where d1 is Element of D : for x being set st x in rng (L1 | A3) holds
( x <> d1 & [x,d1] in R )  }  by A13, A19, A22;
hence  (L1 | A1) . x = (L2 | A1) . x by A22, A24, A23, A25, FUNCT_1:49; ::_thesis: verum
end;
 dom (L1 | A1) = A1 by A13, A19, RELAT_1:62;
hence  L1 | A1 = L2 | A1 by A20, A21, FUNCT_1:2; ::_thesis: verum
end;
 for A1 being Ordinal holds S3[A1] from ORDINAL1:sch_2(A17);
then A26: L1 | A = L2 | A ;
 L2 = L2 | A by A16, RELAT_1:68;
hence  x = y by A12, A15, A26, A14; ::_thesis: verum
end;
 {} in {{}} by TARSKI:def_1;
then A27: not {} in M by XBOOLE_0:def_5;
A28: for X being set st X in bool D & X <> {} holds
g . X in X
proof
let X be set ; ::_thesis: ( X in bool D & X <> {} implies g . X in X )
assume that
A29: X in bool D and
A30: X <> {} ; ::_thesis: g . X in X
 not X in {{}} by A30, TARSKI:def_1;
then A31: X in M by A29, XBOOLE_0:def_5;
 the Choice_Function of M . X = g . X by A10, A29, A30;
hence  g . X in X by A27, A31, Def1; ::_thesis: verum
end;
defpred S3[ Ordinal] means S2[$1,D];
 {} c= D by XBOOLE_1:2;
then A32: g . {} = D by A10;
A33: now__::_thesis:_for_A,_B_being_Ordinal
for_L1,_L2_being_T-Sequence_st_dom_L1_=_A_&_(_for_C_being_Ordinal
for_L_being_T-Sequence_st_C_in_A_&_L_=_L1_|_C_holds_
L1_._C_=_g_.__{__d2_where_d2_is_Element_of_D_:_for_x_being_set_st_x_in_rng_L_holds_
(_x_<>_d2_&_[x,d2]_in_R_)__}__)_&_dom_L2_=_B_&_(_for_C_being_Ordinal
for_L_being_T-Sequence_st_C_in_B_&_L_=_L2_|_C_holds_
L2_._C_=_g_.__{__d2_where_d2_is_Element_of_D_:_for_x_being_set_st_x_in_rng_L_holds_
(_x_<>_d2_&_[x,d2]_in_R_)__}__)_holds_
for_C_being_Ordinal_st_C_c=_A_&_C_c=_B_holds_
L1_|_C_=_L2_|_C
let A, B be Ordinal; ::_thesis: for L1, L2 being T-Sequence st dom L1 = A & ( for C being Ordinal
for L being T-Sequence st C in A & L = L1 | C holds
L1 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) & dom L2 = B & ( for C being Ordinal
for L being T-Sequence st C in B & L = L2 | C holds
L2 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) holds
for C being Ordinal st C c= A & C c= B holds
L1 | C = L2 | C
let L1, L2 be T-Sequence; ::_thesis: ( dom L1 = A & ( for C being Ordinal
for L being T-Sequence st C in A & L = L1 | C holds
L1 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) & dom L2 = B & ( for C being Ordinal
for L being T-Sequence st C in B & L = L2 | C holds
L2 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) implies for C being Ordinal st C c= A & C c= B holds
L1 | C = L2 | C )
assume that
A34: ( dom L1 = A & ( for C being Ordinal
for L being T-Sequence st C in A & L = L1 | C holds
L1 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) ) and
A35: ( dom L2 = B & ( for C being Ordinal
for L being T-Sequence st C in B & L = L2 | C holds
L2 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) ) ; ::_thesis: for C being Ordinal st C c= A & C c= B holds
L1 | C = L2 | C
let C be Ordinal; ::_thesis: ( C c= A & C c= B implies L1 | C = L2 | C )
assume that
A36: C c= A and
A37: C c= B ; ::_thesis: L1 | C = L2 | C
defpred S4[ Ordinal] means ( $1 c= C implies L1 | $1 = L2 | $1 );
A38: for A1 being Ordinal st ( for A2 being Ordinal st A2 in A1 holds
S4[A2] ) holds
S4[A1]
proof
let A1 be Ordinal; ::_thesis: ( ( for A2 being Ordinal st A2 in A1 holds
S4[A2] ) implies S4[A1] )
assume that
A39: for A2 being Ordinal st A2 in A1 & A2 c= C holds
L1 | A2 = L2 | A2 and
A40: A1 c= C ; ::_thesis: L1 | A1 = L2 | A1
A41: dom (L2 | A1) = A1 by A35, A37, A40, RELAT_1:62, XBOOLE_1:1;
A42: now__::_thesis:_for_x_being_set_st_x_in_A1_holds_
(L1_|_A1)_._x_=_(L2_|_A1)_._x
let x be set ; ::_thesis: ( x in A1 implies (L1 | A1) . x = (L2 | A1) . x )
assume A43: x in A1 ; ::_thesis: (L1 | A1) . x = (L2 | A1) . x
then reconsider A3 = x as Ordinal ;
A44: L1 . x = (L1 | A1) . x by A43, FUNCT_1:49;
 A3 c= C by A40, A43, ORDINAL1:def_2;
then A45: L1 | A3 = L2 | A3 by A39, A43;
A46: A3 in C by A40, A43;
then A47: L2 . A3 = g .  {  d2 where d2 is Element of D : for x being set st x in rng (L2 | A3) holds
( x <> d2 & [x,d2] in R )  }  by A35, A37;
 L1 . A3 = g .  {  d1 where d1 is Element of D : for x being set st x in rng (L1 | A3) holds
( x <> d1 & [x,d1] in R )  }  by A34, A36, A46;
hence  (L1 | A1) . x = (L2 | A1) . x by A43, A45, A44, A47, FUNCT_1:49; ::_thesis: verum
end;
 dom (L1 | A1) = A1 by A34, A36, A40, RELAT_1:62, XBOOLE_1:1;
hence  L1 | A1 = L2 | A1 by A41, A42, FUNCT_1:2; ::_thesis: verum
end;
 for A1 being Ordinal holds S4[A1] from ORDINAL1:sch_2(A38);
hence  L1 | C = L2 | C ; ::_thesis: verum
end;
A48: for d being Element of D
for A, B being Ordinal st S2[A,d] & S2[B,d] holds
A = B
proof
let d be Element of D; ::_thesis: for A, B being Ordinal st S2[A,d] & S2[B,d] holds
A = B
let A, B be Ordinal; ::_thesis: ( S2[A,d] & S2[B,d] implies A = B )
given L1 being T-Sequence such that A49: d = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  and
A50: ( dom L1 = A & ( for C being Ordinal
for L being T-Sequence st C in A & L = L1 | C holds
L1 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) ) ; ::_thesis: ( not S2[B,d] or A = B )
given L2 being T-Sequence such that A51: d = g .  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  and
A52: ( dom L2 = B & ( for C being Ordinal
for L being T-Sequence st C in B & L = L2 | C holds
L2 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) ) ; ::_thesis: A = B
A53: now__::_thesis:_not_B_in_A
set Y =  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ;
set X =  {  d1 where d1 is Element of D : for x being set st x in rng (L1 | B) holds
( x <> d1 & [x,d1] in R )  }  ;
A54:  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  or x in D )
assume  x in  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ; ::_thesis: x in D
then  ex d1 being Element of D st
( x = d1 & ( for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence  x in D ; ::_thesis: verum
end;
assume A55: B in A ; ::_thesis: contradiction
then  B c= A by ORDINAL1:def_2;
then A56: L1 | B = L2 | B by A33, A50, A52
.= L2 by A52, RELAT_1:68 ;
 L1 . B = g .  {  d1 where d1 is Element of D : for x being set st x in rng (L1 | B) holds
( x <> d1 & [x,d1] in R )  }  by A50, A55;
then A57: d in rng L1 by A50, A51, A55, A56, FUNCT_1:def_3;
A58: now__::_thesis:_not__{__d1_where_d1_is_Element_of_D_:_for_x_being_set_st_x_in_rng_L1_holds_
(_x_<>_d1_&_[x,d1]_in_R_)__}__<>_{}
assume A59:  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  <> {} ; ::_thesis: contradiction
then  not  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  in {{}} by TARSKI:def_1;
then A60:  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  in M by A54, XBOOLE_0:def_5;
 g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  = the Choice_Function of M .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  by A10, A54, A59;
then  d in  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  by A27, A49, A60, Def1;
then  ex d1 being Element of D st
( d = d1 & ( for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence  contradiction by A57; ::_thesis: verum
end;
A61: not d in d ;
 S1[ {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ,g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ] by A10, A54;
hence  contradiction by A49, A61, A58; ::_thesis: verum
end;
now__::_thesis:_not_A_in_B
set Y =  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  ;
set X =  {  d1 where d1 is Element of D : for x being set st x in rng (L2 | A) holds
( x <> d1 & [x,d1] in R )  }  ;
A62:  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  or x in D )
assume  x in  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  ; ::_thesis: x in D
then  ex d1 being Element of D st
( x = d1 & ( for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence  x in D ; ::_thesis: verum
end;
assume A63: A in B ; ::_thesis: contradiction
then  A c= B by ORDINAL1:def_2;
then A64: L2 | A = L1 | A by A33, A50, A52
.= L1 by A50, RELAT_1:68 ;
 L2 . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng (L2 | A) holds
( x <> d1 & [x,d1] in R )  }  by A52, A63;
then A65: d in rng L2 by A49, A52, A63, A64, FUNCT_1:def_3;
A66: now__::_thesis:_not__{__d1_where_d1_is_Element_of_D_:_for_x_being_set_st_x_in_rng_L2_holds_
(_x_<>_d1_&_[x,d1]_in_R_)__}__<>_{}
assume A67:  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  <> {} ; ::_thesis: contradiction
then  not  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  in {{}} by TARSKI:def_1;
then A68:  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  in M by A62, XBOOLE_0:def_5;
 g .  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  = the Choice_Function of M .  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  by A10, A62, A67;
then  d in  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  by A27, A51, A68, Def1;
then  ex d1 being Element of D st
( d = d1 & ( for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence  contradiction by A65; ::_thesis: verum
end;
A69: not d in d ;
 S1[ {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  ,g .  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  ] by A10, A62;
hence  contradiction by A51, A69, A66; ::_thesis: verum
end;
hence  A = B by A53, ORDINAL1:14; ::_thesis: verum
end;
A70: ex A being Ordinal st S3[A]
proof
defpred S4[ set , set ] means  ex A being Ordinal st
( $2 = A & S2[A,$1] );
defpred S5[ Ordinal] means  ex d being Element of D st S2[$1,d];
assume A71: for A being Ordinal holds not S2[A,D] ; ::_thesis: contradiction
A72: for A being Ordinal st ( for B being Ordinal st B in A holds
S5[B] ) holds
S5[A]
proof
defpred S6[ set , set ] means  ex C being Ordinal st
( $1 = C & S2[C,$2] );
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S5[B] ) implies S5[A] )
assume A73: for B being Ordinal st B in A holds
ex d being Element of D st S2[B,d] ; ::_thesis: S5[A]
A74: for x being set st x in A holds
ex y being set st S6[x,y]
proof
let x be set ; ::_thesis: ( x in A implies ex y being set st S6[x,y] )
assume A75: x in A ; ::_thesis: ex y being set st S6[x,y]
then reconsider C = x as Ordinal ;
consider d being Element of D such that
A76: S2[C,d] by A73, A75;
reconsider y = d as set ;
take  y ; ::_thesis: S6[x,y]
take  C ; ::_thesis: ( x = C & S2[C,y] )
thus  ( x = C & S2[C,y] ) by A76; ::_thesis: verum
end;
A77: for x, y, z being set st x in A & S6[x,y] & S6[x,z] holds
y = z by A11;
consider h being Function such that
A78: ( dom h = A & ( for x being set st x in A holds
S6[x,h . x] ) ) from FUNCT_1:sch_2(A77, A74);
reconsider h = h as T-Sequence by A78, ORDINAL1:def_7;
set X =  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  ;
A79:  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  or x in D )
assume  x in  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  ; ::_thesis: x in D
then  ex d1 being Element of D st
( x = d1 & ( for x being set st x in rng h holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence  x in D ; ::_thesis: verum
end;
A80: S2[A,g .  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  ]
proof
take  h ; ::_thesis: ( g .  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  = g .  {  d where d is Element of D : for x being set st x in rng h holds
( x <> d & [x,d] in R )  }  & dom h = A & ( for A being Ordinal
for L1 being T-Sequence st A in A & L1 = h | A holds
h . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ) )
thus  ( g .  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  = g .  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  & dom h = A ) by A78; ::_thesis: for A being Ordinal
for L1 being T-Sequence st A in A & L1 = h | A holds
h . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }
let B be Ordinal; ::_thesis: for L1 being T-Sequence st B in A & L1 = h | B holds
h . B = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }
let L be T-Sequence; ::_thesis: ( B in A & L = h | B implies h . B = g .  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  )
assume that
A81: B in A and
A82: L = h | B ; ::_thesis: h . B = g .  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }
 ex C being Ordinal st
( B = C & S2[C,h . B] ) by A78, A81;
then consider L1 being T-Sequence such that
A83: h . B = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  and
A84: ( dom L1 = B & ( for C being Ordinal
for L being T-Sequence st C in B & L = L1 | C holds
L1 . C = g .  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  ) ) ;
A85: for x being set st x in B holds
L1 . x = (h | B) . x
proof
let x be set ; ::_thesis: ( x in B implies L1 . x = (h | B) . x )
assume A86: x in B ; ::_thesis: L1 . x = (h | B) . x
then reconsider A1 = x as Ordinal ;
A87: (h | B) . x = h . x by A86, FUNCT_1:49;
A88: S2[A1,L1 . x]
proof
reconsider K = L1 | A1 as T-Sequence ;
take  K ; ::_thesis: ( L1 . x = g .  {  d where d is Element of D : for x being set st x in rng K holds
( x <> d & [x,d] in R )  }  & dom K = A1 & ( for A being Ordinal
for L1 being T-Sequence st A in A1 & L1 = K | A holds
K . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ) )
thus  L1 . x = g .  {  d1 where d1 is Element of D : for x being set st x in rng K holds
( x <> d1 & [x,d1] in R )  }  by A84, A86; ::_thesis: ( dom K = A1 & ( for A being Ordinal
for L1 being T-Sequence st A in A1 & L1 = K | A holds
K . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ) )
 A1 c= B by A86, ORDINAL1:def_2;
hence  dom K = A1 by A84, RELAT_1:62; ::_thesis: for A being Ordinal
for L1 being T-Sequence st A in A1 & L1 = K | A holds
K . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }
let A2 be Ordinal; ::_thesis: for L1 being T-Sequence st A2 in A1 & L1 = K | A2 holds
K . A2 = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }
let L2 be T-Sequence; ::_thesis: ( A2 in A1 & L2 = K | A2 implies K . A2 = g .  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  )
assume that
A89: A2 in A1 and
A90: L2 = K | A2 ; ::_thesis: K . A2 = g .  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }
 A2 c= A1 by A89, ORDINAL1:def_2;
then A91: L2 = L1 | A2 by A90, FUNCT_1:51;
 K . A2 = L1 . A2 by A89, FUNCT_1:49;
hence  K . A2 = g .  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  by A84, A86, A89, A91, ORDINAL1:10; ::_thesis: verum
end;
 ex A2 being Ordinal st
( x = A2 & S2[A2,h . x] ) by A78, A81, A86, ORDINAL1:10;
hence  L1 . x = (h | B) . x by A11, A88, A87; ::_thesis: verum
end;
 B c= A by A81, ORDINAL1:def_2;
then  dom (h | B) = B by A78, RELAT_1:62;
then  h | B = L1 by A84, A85, FUNCT_1:2;
hence  h . B = g .  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  by A82, A83; ::_thesis: verum
end;
then   {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  <> {} by A32, A71;
then  g .  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  in  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  by A28, A79;
then reconsider d = g .  {  d1 where d1 is Element of D : for x being set st x in rng h holds
( x <> d1 & [x,d1] in R )  }  as Element of D by A79;
take  d ; ::_thesis: S2[A,d]
thus  S2[A,d] by A80; ::_thesis: verum
end;
A92: for A being Ordinal holds S5[A] from ORDINAL1:sch_2(A72);
A93: for x, y, z being set st S4[x,y] & S4[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( S4[x,y] & S4[x,z] implies y = z )
given A1 being Ordinal such that A94: y = A1 and
A95: S2[A1,x] ; ::_thesis: ( not S4[x,z] or y = z )
consider d1 being Element of D such that
A96: S2[A1,d1] by A92;
given A2 being Ordinal such that A97: z = A2 and
A98: S2[A2,x] ; ::_thesis: y = z
 d1 = x by A11, A95, A96;
hence  y = z by A48, A94, A95, A97, A98; ::_thesis: verum
end;
consider X being set  such that
A99: for x being set holds
( x in X iff ex y being set st
( y in D & S4[y,x] ) ) from TARSKI:sch_1(A93);
 for A being Ordinal holds A in X
proof
let A be Ordinal; ::_thesis: A in X
 ex d being Element of D st S2[A,d] by A92;
hence  A in X by A99; ::_thesis: verum
end;
hence  contradiction by ORDINAL1:26; ::_thesis: verum
end;
consider A being Ordinal such that
A100: ( S3[A] & ( for B being Ordinal st S3[B] holds
A c= B ) ) from ORDINAL1:sch_1(A70);
A101: for L being T-Sequence holds  {  d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R )  }  c= D
proof
let L be T-Sequence; ::_thesis:  {  d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R )  }  c= D
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R )  }  or x in D )
assume  x in  {  d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R )  }  ; ::_thesis: x in D
then  ex d1 being Element of D st
( x = d1 & ( for x being set st x in rng L holds
( x <> d1 & [x,d1] in R ) ) ) ;
hence  x in D ; ::_thesis: verum
end;
 D in bool D by ZFMISC_1:def_1;
then reconsider d = g . D as Element of D by A28;
A102: ( d in D & S2[ {} ,d] )
proof
deffunc H1( set ) ->  set = {} ;
thus  d in D ; ::_thesis: S2[ {} ,d]
consider L being T-Sequence such that
A103: ( dom L = {} & ( for B being Ordinal
for L1 being T-Sequence st B in {} & L1 = L | B holds
L . B = H1(L1) ) ) from ORDINAL1:sch_4();
take  L ; ::_thesis: ( d = g .  {  d where d is Element of D : for x being set st x in rng L holds
( x <> d & [x,d] in R )  }  & dom L = {} & ( for A being Ordinal
for L1 being T-Sequence st A in {} & L1 = L | A holds
L . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ) )
A104: D c=  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  )
assume  x in D ; ::_thesis: x in  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }
then reconsider d = x as Element of D ;
 for x being set st x in rng L holds
( x <> d & [x,d] in R ) by A103, RELAT_1:42;
hence  x in  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  ; ::_thesis: verum
end;
  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  c= D by A101;
hence  d = g .  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  by A104, XBOOLE_0:def_10; ::_thesis: ( dom L = {} & ( for A being Ordinal
for L1 being T-Sequence st A in {} & L1 = L | A holds
L . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ) )
thus  dom L = {} by A103; ::_thesis: for A being Ordinal
for L1 being T-Sequence st A in {} & L1 = L | A holds
L . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }
thus  for A being Ordinal
for L1 being T-Sequence st A in {} & L1 = L | A holds
L . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ; ::_thesis: verum
end;
A105: {} c= A ;
defpred S4[ set ] means  ex B being Ordinal st
( B in A & S2[B,$1] );
consider X being set  such that
A106: for x being set holds
( x in X iff ( x in D & S4[x] ) ) from XBOOLE_0:sch_1();
 for Y being set holds not Y in Y ;
then  d <> D ;
then  {} <> A by A11, A100, A102;
then  {} c< A by A105, XBOOLE_0:def_8;
then  {} in A by ORDINAL1:11;
then reconsider X = X as non empty set by A106, A102;
consider L being T-Sequence such that
A107: D = g .  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  and
A108: ( dom L = A & ( for B being Ordinal
for L1 being T-Sequence st B in A & L1 = L | B holds
L . B = g .  {  d2 where d2 is Element of D : for x being set st x in rng L1 holds
( x <> d2 & [x,d2] in R )  }  ) ) by A100;
 R is transitive by A2, A4, RELAT_2:def_16;
then A109: R |_2 X is transitive by WELLORD1:17;
A110: rng L c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng L or z in X )
assume  z in rng L ; ::_thesis: z in X
then consider y being set  such that
A111: y in dom L and
A112: z = L . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A111;
set Z =  {  d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R )  }  ;
A113:  {  d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R )  }  c= D by A101;
A114: S2[y,z]
proof
reconsider K = L | y as T-Sequence ;
take  K ; ::_thesis: ( z = g .  {  d where d is Element of D : for x being set st x in rng K holds
( x <> d & [x,d] in R )  }  & dom K = y & ( for A being Ordinal
for L1 being T-Sequence st A in y & L1 = K | A holds
K . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ) )
thus  z = g .  {  d2 where d2 is Element of D : for x being set st x in rng K holds
( x <> d2 & [x,d2] in R )  }  by A108, A111, A112; ::_thesis: ( dom K = y & ( for A being Ordinal
for L1 being T-Sequence st A in y & L1 = K | A holds
K . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ) )
 y c= dom L by A111, ORDINAL1:def_2;
hence A115: dom K = y by RELAT_1:62; ::_thesis: for A being Ordinal
for L1 being T-Sequence st A in y & L1 = K | A holds
K . A = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }
let B be Ordinal; ::_thesis: for L1 being T-Sequence st B in y & L1 = K | B holds
K . B = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }
let L1 be T-Sequence; ::_thesis: ( B in y & L1 = K | B implies K . B = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  )
assume that
A116: B in y and
A117: L1 = K | B ; ::_thesis: K . B = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }
 B c= y by A116, ORDINAL1:def_2;
then A118: L1 = L | B by A117, FUNCT_1:51;
 K . B = L . B by A115, A116, FUNCT_1:47;
hence  K . B = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  by A108, A111, A116, A118, ORDINAL1:10; ::_thesis: verum
end;
now__::_thesis:_not__{__d2_where_d2_is_Element_of_D_:_for_x_being_set_st_x_in_rng_(L_|_y)_holds_
(_x_<>_d2_&_[x,d2]_in_R_)__}__=_{}
assume   {  d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R )  }  = {} ; ::_thesis: contradiction
then  z = D by A32, A108, A111, A112;
then  dom L c= y by A100, A108, A114;
hence  contradiction by A111, ORDINAL1:5; ::_thesis: verum
end;
then  g .  {  d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R )  }  in  {  d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R )  }  by A28, A113;
then  z in  {  d2 where d2 is Element of D : for x being set st x in rng (L | y) holds
( x <> d2 & [x,d2] in R )  }  by A108, A111, A112;
hence  z in X by A106, A108, A111, A114, A113; ::_thesis: verum
end;
A119: R |_2 X is connected
proof
let x be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds
( not x in field (R |_2 X) or not b1 in field (R |_2 X) or x = b1 or [x,b1] in R |_2 X or [b1,x] in R |_2 X )
let y be set ; ::_thesis: ( not x in field (R |_2 X) or not y in field (R |_2 X) or x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
assume that
A120: x in field (R |_2 X) and
A121: y in field (R |_2 X) ; ::_thesis: ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
A122: x in X by A120, WELLORD1:12;
then consider A1 being Ordinal such that
 A1 in A and
A123: S2[A1,x] by A106;
A124: y in X by A121, WELLORD1:12;
then consider A2 being Ordinal such that
 A2 in A and
A125: S2[A2,y] by A106;
reconsider x9 = x, y9 = y as Element of D by A106, A122, A124;
consider L1 being T-Sequence such that
A126: x9 = g .  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  and
A127: ( dom L1 = A1 & ( for C being Ordinal
for L being T-Sequence st C in A1 & L = L1 | C holds
L1 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) ) by A123;
consider L2 being T-Sequence such that
A128: y9 = g .  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  and
A129: ( dom L2 = A2 & ( for C being Ordinal
for L being T-Sequence st C in A2 & L = L2 | C holds
L2 . C = g .  {  d2 where d2 is Element of D : for x being set st x in rng L holds
( x <> d2 & [x,d2] in R )  }  ) ) by A125;
A130: [x,y] in [:X,X:] by A122, A124, ZFMISC_1:87;
A131: now__::_thesis:_(_A1_in_A2_&_not_x_=_y_&_not_[x,y]_in_R_|_2_X_implies_[y,x]_in_R_|_2_X_)
set Y =  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  ;
set Z =  {  d1 where d1 is Element of D : for x being set st x in rng (L2 | A1) holds
( x <> d1 & [x,d1] in R )  }  ;
 not y9 in y9 ;
then A132:  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  <> {} by A32, A128;
  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  c= D by A101;
then  y9 in  {  d1 where d1 is Element of D : for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R )  }  by A28, A128, A132;
then A133: ex d1 being Element of D st
( y9 = d1 & ( for x being set st x in rng L2 holds
( x <> d1 & [x,d1] in R ) ) ) ;
assume A134: A1 in A2 ; ::_thesis: ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
then  A1 c= A2 by ORDINAL1:def_2;
then A135: L2 | A1 = L1 | A1 by A33, A127, A129
.= L1 by A127, RELAT_1:68 ;
 L2 . A1 = g .  {  d1 where d1 is Element of D : for x being set st x in rng (L2 | A1) holds
( x <> d1 & [x,d1] in R )  }  by A129, A134;
then  x9 in rng L2 by A126, A129, A134, A135, FUNCT_1:def_3;
then  [x,y] in R by A133;
hence  ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X ) by A130, XBOOLE_0:def_4; ::_thesis: verum
end;
A136: [y,x] in [:X,X:] by A122, A124, ZFMISC_1:87;
A137: now__::_thesis:_(_A2_in_A1_&_not_x_=_y_&_not_[x,y]_in_R_|_2_X_implies_[y,x]_in_R_|_2_X_)
set Y =  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  ;
set Z =  {  d1 where d1 is Element of D : for x being set st x in rng (L1 | A2) holds
( x <> d1 & [x,d1] in R )  }  ;
 for d1 being Element of D holds not d1 in d1 ;
then A138:  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  <> {} by A32, A126;
  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  c= D by A101;
then  x9 in  {  d1 where d1 is Element of D : for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R )  }  by A28, A126, A138;
then A139: ex d1 being Element of D st
( x9 = d1 & ( for x being set st x in rng L1 holds
( x <> d1 & [x,d1] in R ) ) ) ;
assume A140: A2 in A1 ; ::_thesis: ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
then  A2 c= A1 by ORDINAL1:def_2;
then A141: L1 | A2 = L2 | A2 by A33, A127, A129
.= L2 by A129, RELAT_1:68 ;
 L1 . A2 = g .  {  d1 where d1 is Element of D : for x being set st x in rng (L1 | A2) holds
( x <> d1 & [x,d1] in R )  }  by A127, A140;
then  y9 in rng L1 by A127, A128, A140, A141, FUNCT_1:def_3;
then  [y,x] in R by A139;
hence  ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X ) by A136, XBOOLE_0:def_4; ::_thesis: verum
end;
 ( A1 = A2 & not x = y & not [x,y] in R |_2 X implies [y,x] in R |_2 X ) by A11, A123, A125;
hence  ( x = y or [x,y] in R |_2 X or [y,x] in R |_2 X ) by A131, A137, ORDINAL1:14; ::_thesis: verum
end;
 R is antisymmetric by A3, A4, RELAT_2:def_12;
then A142: R |_2 X is antisymmetric ;
set Z =  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  ;
A143: X c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in D )
thus  ( not x in X or x in D ) by A106; ::_thesis: verum
end;
 R is reflexive by A1, A4, RELAT_2:def_9;
then  R |_2 X is reflexive by WELLORD1:15;
then  R |_2 X is being_linear-order by A109, A142, A119, Def5;
then consider x being set  such that
A144: x in D and
A145: for y being set st y in X holds
[y,x] in R by A5, A6, A143, Def9;
take  x ; ::_thesis: x is_maximal_in R
thus  x in field R by A4, A6, A144; :: according to ORDERS_1:def_11 ::_thesis: for y being set holds
( not y in field R or not y <> x or not [x,y] in R )
let y be set ; ::_thesis: ( not y in field R or not y <> x or not [x,y] in R )
assume that
A146: y in field R and
A147: y <> x and
A148: [x,y] in R ; ::_thesis: contradiction
reconsider y9 = y as Element of D by A4, A6, A146;
A149: now__::_thesis:_not_y_in_X
assume  y in X ; ::_thesis: contradiction
then  [y,x] in R by A145;
hence  contradiction by A3, A4, A6, A144, A146, A147, A148, RELAT_2:def_4; ::_thesis: verum
end;
now__::_thesis:_for_z_being_set_st_z_in_rng_L_holds_
(_z_<>_y9_&_[z,y]_in_R_)
let z be set ; ::_thesis: ( z in rng L implies ( z <> y9 & [z,y] in R ) )
assume A150: z in rng L ; ::_thesis: ( z <> y9 & [z,y] in R )
then reconsider z9 = z as Element of X by A110;
thus  z <> y9 by A110, A149, A150; ::_thesis: [z,y] in R
A151: [z9,x] in R by A145;
 z in D by A106, A110, A150;
hence  [z,y] in R by A2, A4, A6, A144, A146, A148, A151, RELAT_2:def_8; ::_thesis: verum
end;
then A152: y in  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  ;
  {  d1 where d1 is Element of D : for x being set st x in rng L holds
( x <> d1 & [x,d1] in R )  }  c= D by A101;
hence  contradiction by A28, A107, A152, ORDINAL1:5; ::_thesis: verum
end;

theorem Th64: :: ORDERS_1:64
for R being Relation
for X being set st R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R holds
ex x being set st x is_minimal_in R
proof
let R be Relation; ::_thesis: for X being set st R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R holds
ex x being set st x is_minimal_in R
let X be set ; ::_thesis: ( R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R implies ex x being set st x is_minimal_in R )
assume that
A1: R partially_orders X and
A2: field R = X and
A3: X has_lower_Zorn_property_wrt R ; ::_thesis: ex x being set st x is_minimal_in R
 R = (R ~) ~ ;
then A4: X has_upper_Zorn_property_wrt R ~ by A3, Th51;
 field (R ~) = X by A2, RELAT_1:21;
then consider x being set  such that
A5: x is_maximal_in R ~ by A1, A4, Th41, Th63;
take  x ; ::_thesis: x is_minimal_in R
thus  x is_minimal_in R by A5, Th59; ::_thesis: verum
end;

theorem Th65: :: ORDERS_1:65
for X being set st X <> {} & ( for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) ) holds
ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) )
proof
let X be set ; ::_thesis: ( X <> {} & ( for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) ) implies ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) ) )
assume that
A1: X <> {} and
A2: for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) ; ::_thesis: ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) )
reconsider D = X as non empty set by A1;
set R = RelIncl D;
A3: D has_upper_Zorn_property_wrt RelIncl D
proof
let Z be set ; :: according to ORDERS_1:def_9 ::_thesis: ( Z c= D & (RelIncl D) |_2 Z is being_linear-order implies ex x being set st
( x in D & ( for y being set st y in Z holds
[y,x] in RelIncl D ) ) )
assume that
A4: Z c= D and
A5: (RelIncl D) |_2 Z is being_linear-order ; ::_thesis: ex x being set st
( x in D & ( for y being set st y in Z holds
[y,x] in RelIncl D ) )
set Q = (RelIncl D) |_2 Z;
A6: Z c= field ((RelIncl D) |_2 Z)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in field ((RelIncl D) |_2 Z) )
assume A7: x in Z ; ::_thesis: x in field ((RelIncl D) |_2 Z)
then A8: [x,x] in [:Z,Z:] by ZFMISC_1:87;
 [x,x] in RelIncl D by A4, A7, WELLORD2:def_1;
then  [x,x] in (RelIncl D) |_2 Z by A8, XBOOLE_0:def_4;
hence  x in field ((RelIncl D) |_2 Z) by RELAT_1:15; ::_thesis: verum
end;
 (RelIncl D) |_2 Z is connected by A5, Def5;
then A9: (RelIncl D) |_2 Z is_connected_in field ((RelIncl D) |_2 Z) by RELAT_2:def_14;
 Z is c=-linear
proof
let X1 be set ; :: according to ORDINAL1:def_8 ::_thesis: for b1 being set holds
( not X1 in Z or not b1 in Z or X1,b1 are_c=-comparable )
let X2 be set ; ::_thesis: ( not X1 in Z or not X2 in Z or X1,X2 are_c=-comparable )
assume that
A10: X1 in Z and
A11: X2 in Z ; ::_thesis: X1,X2 are_c=-comparable
 ( not X1 <> X2 or [X1,X2] in (RelIncl D) |_2 Z or [X2,X1] in (RelIncl D) |_2 Z ) by A9, A6, A10, A11, RELAT_2:def_6;
then  ( not X1 <> X2 or [X1,X2] in RelIncl D or [X2,X1] in RelIncl D ) by XBOOLE_0:def_4;
hence  ( X1 c= X2 or X2 c= X1 ) by A4, A10, A11, WELLORD2:def_1; :: according to XBOOLE_0:def_9 ::_thesis: verum
end;
then consider Y being set  such that
A12: Y in X and
A13: for X1 being set st X1 in Z holds
X1 c= Y by A2, A4;
take x = Y; ::_thesis: ( x in D & ( for y being set st y in Z holds
[y,x] in RelIncl D ) )
thus  x in D by A12; ::_thesis: for y being set st y in Z holds
[y,x] in RelIncl D
let y be set ; ::_thesis: ( y in Z implies [y,x] in RelIncl D )
assume A14: y in Z ; ::_thesis: [y,x] in RelIncl D
then  y c= Y by A13;
hence  [y,x] in RelIncl D by A4, A12, A14, WELLORD2:def_1; ::_thesis: verum
end;
A15: field (RelIncl D) = D by WELLORD2:def_1;
A16: RelIncl D is_antisymmetric_in D by A15, RELAT_2:def_12;
A17: RelIncl D is_transitive_in D by A15, RELAT_2:def_16;
 RelIncl D is_reflexive_in D by A15, RELAT_2:def_9;
then  RelIncl D partially_orders D by A17, A16, Def7;
then consider x being set  such that
A18: x is_maximal_in RelIncl D by A15, A3, Th63;
take Y = x; ::_thesis: ( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) )
A19: Y in field (RelIncl D) by A18, Def11;
thus  Y in X by A15, A18, Def11; ::_thesis: for Z being set st Z in X & Z <> Y holds
not Y c= Z
let Z be set ; ::_thesis: ( Z in X & Z <> Y implies not Y c= Z )
assume that
A20: Z in X and
A21: Z <> Y ; ::_thesis: not Y c= Z
 not [Y,Z] in RelIncl D by A15, A18, A20, A21, Def11;
hence  not Y c= Z by A15, A19, A20, WELLORD2:def_1; ::_thesis: verum
end;

theorem Th66: :: ORDERS_1:66
for X being set st X <> {} & ( for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
Y c= X1 ) ) ) holds
ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) )
proof
let X be set ; ::_thesis: ( X <> {} & ( for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
Y c= X1 ) ) ) implies ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) ) )
assume that
A1: X <> {} and
A2: for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
Y c= X1 ) ) ; ::_thesis: ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) )
reconsider D = X as non empty set by A1;
set R = (RelIncl D) ~ ;
A3: for x being set st x in D holds
[x,x] in (RelIncl D) ~
proof
let x be set ; ::_thesis: ( x in D implies [x,x] in (RelIncl D) ~ )
 ( x in D implies [x,x] in RelIncl D ) by WELLORD2:def_1;
hence  ( x in D implies [x,x] in (RelIncl D) ~ ) by RELAT_1:def_7; ::_thesis: verum
end;
A4: D has_upper_Zorn_property_wrt (RelIncl D) ~
proof
let Z be set ; :: according to ORDERS_1:def_9 ::_thesis: ( Z c= D & ((RelIncl D) ~) |_2 Z is being_linear-order implies ex x being set st
( x in D & ( for y being set st y in Z holds
[y,x] in (RelIncl D) ~ ) ) )
assume that
A5: Z c= D and
A6: ((RelIncl D) ~) |_2 Z is being_linear-order ; ::_thesis: ex x being set st
( x in D & ( for y being set st y in Z holds
[y,x] in (RelIncl D) ~ ) )
set Q = ((RelIncl D) ~) |_2 Z;
A7: Z c= field (((RelIncl D) ~) |_2 Z)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in field (((RelIncl D) ~) |_2 Z) )
assume A8: x in Z ; ::_thesis: x in field (((RelIncl D) ~) |_2 Z)
then A9: [x,x] in [:Z,Z:] by ZFMISC_1:87;
 [x,x] in (RelIncl D) ~ by A3, A5, A8;
then  [x,x] in ((RelIncl D) ~) |_2 Z by A9, XBOOLE_0:def_4;
hence  x in field (((RelIncl D) ~) |_2 Z) by RELAT_1:15; ::_thesis: verum
end;
 ((RelIncl D) ~) |_2 Z is connected by A6, Def5;
then A10: ((RelIncl D) ~) |_2 Z is_connected_in field (((RelIncl D) ~) |_2 Z) by RELAT_2:def_14;
 Z is c=-linear
proof
let X1 be set ; :: according to ORDINAL1:def_8 ::_thesis: for b1 being set holds
( not X1 in Z or not b1 in Z or X1,b1 are_c=-comparable )
let X2 be set ; ::_thesis: ( not X1 in Z or not X2 in Z or X1,X2 are_c=-comparable )
assume that
A11: X1 in Z and
A12: X2 in Z ; ::_thesis: X1,X2 are_c=-comparable
 ( not X1 <> X2 or [X1,X2] in ((RelIncl D) ~) |_2 Z or [X2,X1] in ((RelIncl D) ~) |_2 Z ) by A10, A7, A11, A12, RELAT_2:def_6;
then  ( not X1 <> X2 or [X1,X2] in (RelIncl D) ~ or [X2,X1] in (RelIncl D) ~ ) by XBOOLE_0:def_4;
then  ( not X1 <> X2 or [X1,X2] in RelIncl D or [X2,X1] in RelIncl D ) by RELAT_1:def_7;
hence  ( X1 c= X2 or X2 c= X1 ) by A5, A11, A12, WELLORD2:def_1; :: according to XBOOLE_0:def_9 ::_thesis: verum
end;
then consider Y being set  such that
A13: Y in X and
A14: for X1 being set st X1 in Z holds
Y c= X1 by A2, A5;
take x = Y; ::_thesis: ( x in D & ( for y being set st y in Z holds
[y,x] in (RelIncl D) ~ ) )
thus  x in D by A13; ::_thesis: for y being set st y in Z holds
[y,x] in (RelIncl D) ~
let y be set ; ::_thesis: ( y in Z implies [y,x] in (RelIncl D) ~ )
assume A15: y in Z ; ::_thesis: [y,x] in (RelIncl D) ~
then  Y c= y by A14;
then  [Y,y] in RelIncl D by A5, A13, A15, WELLORD2:def_1;
hence  [y,x] in (RelIncl D) ~ by RELAT_1:def_7; ::_thesis: verum
end;
A16: field ((RelIncl D) ~) = field (RelIncl D) by RELAT_1:21
.= D by WELLORD2:def_1 ;
A17: field (RelIncl D) = D by WELLORD2:def_1;
 RelIncl D is_antisymmetric_in D by A17, RELAT_2:def_12;
then A18: (RelIncl D) ~ is_antisymmetric_in D by Lm13;
 RelIncl D is_transitive_in D by A17, RELAT_2:def_16;
then A19: (RelIncl D) ~ is_transitive_in D by Lm12;
 RelIncl D is_reflexive_in D by A17, RELAT_2:def_9;
then  (RelIncl D) ~ is_reflexive_in D by Lm11;
then  (RelIncl D) ~ partially_orders D by A19, A18, Def7;
then consider x being set  such that
A20: x is_maximal_in (RelIncl D) ~ by A16, A4, Th63;
take Y = x; ::_thesis: ( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) )
A21: Y in field ((RelIncl D) ~) by A20, Def11;
thus  Y in X by A16, A20, Def11; ::_thesis: for Z being set st Z in X & Z <> Y holds
not Z c= Y
let Z be set ; ::_thesis: ( Z in X & Z <> Y implies not Z c= Y )
assume that
A22: Z in X and
A23: Z <> Y ; ::_thesis: not Z c= Y
 not [Y,Z] in (RelIncl D) ~ by A16, A20, A22, A23, Def11;
then  not [Z,Y] in RelIncl D by RELAT_1:def_7;
hence  not Z c= Y by A16, A21, A22, WELLORD2:def_1; ::_thesis: verum
end;

theorem Th67: :: ORDERS_1:67
for X being set st X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
union Z in X ) holds
ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) )
proof
let X be set ; ::_thesis: ( X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
union Z in X ) implies ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) ) )
assume that
A1: X <> {} and
A2: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
union Z in X ; ::_thesis: ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) )
 for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
set x = the Element of X;
let Z be set ; ::_thesis: ( Z c= X & Z is c=-linear implies ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that
A3: Z c= X and
A4: Z is c=-linear ; ::_thesis: ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
 ( Z <> {} or Z = {} ) ;
then consider Y being set  such that
A5: ( ( Y = union Z & Z <> {} ) or ( Y = the Element of X & Z = {} ) ) ;
take  Y ; ::_thesis: ( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
thus  ( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by A1, A2, A3, A4, A5, ZFMISC_1:74; ::_thesis: verum
end;
hence  ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) ) by A1, Th65; ::_thesis: verum
end;

theorem :: ORDERS_1:68
for X being set st X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
meet Z in X ) holds
ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) )
proof
let X be set ; ::_thesis: ( X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
meet Z in X ) implies ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) ) )
assume that
A1: X <> {} and
A2: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
meet Z in X ; ::_thesis: ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) )
 for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
Y c= X1 ) )
proof
set x = the Element of X;
let Z be set ; ::_thesis: ( Z c= X & Z is c=-linear implies ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
Y c= X1 ) ) )
assume that
A3: Z c= X and
A4: Z is c=-linear ; ::_thesis: ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
Y c= X1 ) )
 ( Z <> {} or Z = {} ) ;
then consider Y being set  such that
A5: ( ( Y = meet Z & Z <> {} ) or ( Y = the Element of X & Z = {} ) ) ;
take  Y ; ::_thesis: ( Y in X & ( for X1 being set st X1 in Z holds
Y c= X1 ) )
thus  ( Y in X & ( for X1 being set st X1 in Z holds
Y c= X1 ) ) by A1, A2, A3, A4, A5, SETFAM_1:3; ::_thesis: verum
end;
hence  ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) ) by A1, Th66; ::_thesis: verum
end;

scheme :: ORDERS_1:sch 1
ZornMax{ F1() ->  non empty set , P1[ set , set ] } :
 ex x being Element of F1() st
for y being Element of F1() st x <> y holds
not P1[x,y]
provided
A1: for x being Element of F1() holds P1[x,x] and
A2: for x, y being Element of F1() st P1[x,y] & P1[y,x] holds
x = y and
A3: for x, y, z being Element of F1() st P1[x,y] & P1[y,z] holds
P1[x,z] and
A4: for X being set st X c= F1() & ( for x, y being Element of F1() st x in X & y in X & P1[x,y] holds
P1[y,x] ) holds
ex y being Element of F1() st
for x being Element of F1() st x in X holds
P1[x,y]
proof
consider R being Relation of F1() such that
A5: for x, y being Element of F1() holds
( [x,y] in R iff P1[x,y] ) from RELSET_1:sch_2();
A6: R is_transitive_in F1()
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in F1() or not b1 in F1() or not b2 in F1() or not [x,b1] in R or not [b1,b2] in R or [x,b2] in R )
let y, z be set ; ::_thesis: ( not x in F1() or not y in F1() or not z in F1() or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A7: x in F1() and
A8: y in F1() and
A9: z in F1() ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
reconsider x9 = x, y9 = y, z9 = z as Element of F1() by A7, A8, A9;
assume that
A10: [x,y] in R and
A11: [y,z] in R ; ::_thesis: [x,z] in R
A12: P1[y9,z9] by A5, A11;
 P1[x9,y9] by A5, A10;
then  P1[x9,z9] by A3, A12;
hence  [x,z] in R by A5; ::_thesis: verum
end;
 F1() c= dom R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() or x in dom R )
assume  x in F1() ; ::_thesis: x in dom R
then reconsider x9 = x as Element of F1() ;
 P1[x9,x9] by A1;
then  [x,x] in R by A5;
hence  x in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;
then  dom R = F1() by XBOOLE_0:def_10;
then A13: F1() c= field R by XBOOLE_1:7;
 field R = (dom R) \/ (rng R) ;
then A14: field R = F1() by A13, XBOOLE_0:def_10;
A15: R is_reflexive_in F1()
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in F1() or [x,x] in R )
assume  x in F1() ; ::_thesis: [x,x] in R
then reconsider x9 = x as Element of F1() ;
 P1[x9,x9] by A1;
hence  [x,x] in R by A5; ::_thesis: verum
end;
A16: F1() has_upper_Zorn_property_wrt R
proof
let Y be set ; :: according to ORDERS_1:def_9 ::_thesis: ( Y c= F1() & R |_2 Y is being_linear-order implies ex x being set st
( x in F1() & ( for y being set st y in Y holds
[y,x] in R ) ) )
assume that
A17: Y c= F1() and
A18: R |_2 Y is being_linear-order ; ::_thesis: ex x being set st
( x in F1() & ( for y being set st y in Y holds
[y,x] in R ) )
 for x, y being Element of F1() st x in Y & y in Y & P1[x,y] holds
P1[y,x]
proof
let x, y be Element of F1(); ::_thesis: ( x in Y & y in Y & P1[x,y] implies P1[y,x] )
assume that
A19: x in Y and
A20: y in Y ; ::_thesis: ( P1[x,y] or P1[y,x] )
A21: ( R |_2 Y is reflexive & R |_2 Y is connected ) by A18, Def5;
 Y c= field (R |_2 Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in field (R |_2 Y) )
assume A22: x in Y ; ::_thesis: x in field (R |_2 Y)
then A23: [x,x] in [:Y,Y:] by ZFMISC_1:87;
 [x,x] in R by A15, A17, A22, RELAT_2:def_1;
then  [x,x] in R |_2 Y by A23, XBOOLE_0:def_4;
hence  x in field (R |_2 Y) by RELAT_1:15; ::_thesis: verum
end;
then A24: Y = field ((R |_2 Y) |_2 Y) by A21, Lm5
.= field (R |_2 Y) by WELLORD1:21 ;
then A25: R |_2 Y is_connected_in Y by A21, RELAT_2:def_14;
A26: R |_2 Y is_reflexive_in Y by A21, A24, RELAT_2:def_9;
 ( x = y or x <> y ) ;
then  ( [x,y] in R |_2 Y or [y,x] in R |_2 Y ) by A19, A20, A25, A26, RELAT_2:def_1, RELAT_2:def_6;
then  ( [x,y] in R or [y,x] in R ) by XBOOLE_0:def_4;
hence  ( P1[x,y] or P1[y,x] ) by A5; ::_thesis: verum
end;
then consider y being Element of F1() such that
A27: for x being Element of F1() st x in Y holds
P1[x,y] by A4, A17;
take  y ; ::_thesis: ( y in F1() & ( for y being set st y in Y holds
[y,y] in R ) )
thus  y in F1() ; ::_thesis: for y being set st y in Y holds
[y,y] in R
let x be set ; ::_thesis: ( x in Y implies [x,y] in R )
assume A28: x in Y ; ::_thesis: [x,y] in R
then  P1[x,y] by A17, A27;
hence  [x,y] in R by A5, A17, A28; ::_thesis: verum
end;
 R is_antisymmetric_in F1()
proof
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds
( not x in F1() or not b1 in F1() or not [x,b1] in R or not [b1,x] in R or x = b1 )
let y be set ; ::_thesis: ( not x in F1() or not y in F1() or not [x,y] in R or not [y,x] in R or x = y )
assume that
A29: x in F1() and
A30: y in F1() ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y )
reconsider x9 = x, y9 = y as Element of F1() by A29, A30;
assume that
A31: [x,y] in R and
A32: [y,x] in R ; ::_thesis: x = y
A33: P1[y9,x9] by A5, A32;
 P1[x9,y9] by A5, A31;
hence  x = y by A2, A33; ::_thesis: verum
end;
then  R partially_orders F1() by A15, A6, Def7;
then consider x being set  such that
A34: x is_maximal_in R by A14, A16, Th63;
take  x ; ::_thesis: ( x is Element of F1() & ( for y being Element of F1() st x <> y holds
not P1[x,y] ) )
thus  x is Element of F1() by A14, A34, Def11; ::_thesis: for y being Element of F1() st x <> y holds
not P1[x,y]
let y be Element of F1(); ::_thesis: ( x <> y implies not P1[x,y] )
assume  x <> y ; ::_thesis: P1[x,y]
then A35: not [x,y] in R by A14, A34, Def11;
 x in F1() by A14, A34, Def11;
hence  P1[x,y] by A5, A35; ::_thesis: verum
end;

scheme :: ORDERS_1:sch 2
ZornMin{ F1() ->  non empty set , P1[ set , set ] } :
 ex x being Element of F1() st
for y being Element of F1() st x <> y holds
not P1[y,x]
provided
A1: for x being Element of F1() holds P1[x,x] and
A2: for x, y being Element of F1() st P1[x,y] & P1[y,x] holds
x = y and
A3: for x, y, z being Element of F1() st P1[x,y] & P1[y,z] holds
P1[x,z] and
A4: for X being set st X c= F1() & ( for x, y being Element of F1() st x in X & y in X & P1[x,y] holds
P1[y,x] ) holds
ex y being Element of F1() st
for x being Element of F1() st x in X holds
P1[y,x]
proof
consider R being Relation of F1() such that
A5: for x, y being Element of F1() holds
( [x,y] in R iff P1[x,y] ) from RELSET_1:sch_2();
A6: R is_transitive_in F1()
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in F1() or not b1 in F1() or not b2 in F1() or not [x,b1] in R or not [b1,b2] in R or [x,b2] in R )
let y, z be set ; ::_thesis: ( not x in F1() or not y in F1() or not z in F1() or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A7: x in F1() and
A8: y in F1() and
A9: z in F1() ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
reconsider x9 = x, y9 = y, z9 = z as Element of F1() by A7, A8, A9;
assume that
A10: [x,y] in R and
A11: [y,z] in R ; ::_thesis: [x,z] in R
A12: P1[y9,z9] by A5, A11;
 P1[x9,y9] by A5, A10;
then  P1[x9,z9] by A3, A12;
hence  [x,z] in R by A5; ::_thesis: verum
end;
 F1() c= dom R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() or x in dom R )
assume  x in F1() ; ::_thesis: x in dom R
then reconsider x9 = x as Element of F1() ;
 P1[x9,x9] by A1;
then  [x,x] in R by A5;
hence  x in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;
then  dom R = F1() by XBOOLE_0:def_10;
then A13: F1() c= field R by XBOOLE_1:7;
 field R = (dom R) \/ (rng R) ;
then A14: field R = F1() by A13, XBOOLE_0:def_10;
A15: R is_reflexive_in F1()
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in F1() or [x,x] in R )
assume  x in F1() ; ::_thesis: [x,x] in R
then reconsider x9 = x as Element of F1() ;
 P1[x9,x9] by A1;
hence  [x,x] in R by A5; ::_thesis: verum
end;
A16: F1() has_lower_Zorn_property_wrt R
proof
let Y be set ; :: according to ORDERS_1:def_10 ::_thesis: ( Y c= F1() & R |_2 Y is being_linear-order implies ex x being set st
( x in F1() & ( for y being set st y in Y holds
[x,y] in R ) ) )
assume that
A17: Y c= F1() and
A18: R |_2 Y is being_linear-order ; ::_thesis: ex x being set st
( x in F1() & ( for y being set st y in Y holds
[x,y] in R ) )
 for x, y being Element of F1() st x in Y & y in Y & P1[x,y] holds
P1[y,x]
proof
let x, y be Element of F1(); ::_thesis: ( x in Y & y in Y & P1[x,y] implies P1[y,x] )
assume that
A19: x in Y and
A20: y in Y ; ::_thesis: ( P1[x,y] or P1[y,x] )
A21: ( R |_2 Y is reflexive & R |_2 Y is connected ) by A18, Def5;
 Y c= field (R |_2 Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in field (R |_2 Y) )
assume A22: x in Y ; ::_thesis: x in field (R |_2 Y)
then A23: [x,x] in [:Y,Y:] by ZFMISC_1:87;
 [x,x] in R by A15, A17, A22, RELAT_2:def_1;
then  [x,x] in R |_2 Y by A23, XBOOLE_0:def_4;
hence  x in field (R |_2 Y) by RELAT_1:15; ::_thesis: verum
end;
then A24: Y = field ((R |_2 Y) |_2 Y) by A21, Lm5
.= field (R |_2 Y) by WELLORD1:21 ;
then A25: R |_2 Y is_connected_in Y by A21, RELAT_2:def_14;
A26: R |_2 Y is_reflexive_in Y by A21, A24, RELAT_2:def_9;
 ( x = y or x <> y ) ;
then  ( [x,y] in R |_2 Y or [y,x] in R |_2 Y ) by A19, A20, A25, A26, RELAT_2:def_1, RELAT_2:def_6;
then  ( [x,y] in R or [y,x] in R ) by XBOOLE_0:def_4;
hence  ( P1[x,y] or P1[y,x] ) by A5; ::_thesis: verum
end;
then consider y being Element of F1() such that
A27: for x being Element of F1() st x in Y holds
P1[y,x] by A4, A17;
take  y ; ::_thesis: ( y in F1() & ( for y being set st y in Y holds
[y,y] in R ) )
thus  y in F1() ; ::_thesis: for y being set st y in Y holds
[y,y] in R
let x be set ; ::_thesis: ( x in Y implies [y,x] in R )
assume A28: x in Y ; ::_thesis: [y,x] in R
then  P1[y,x] by A17, A27;
hence  [y,x] in R by A5, A17, A28; ::_thesis: verum
end;
 R is_antisymmetric_in F1()
proof
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds
( not x in F1() or not b1 in F1() or not [x,b1] in R or not [b1,x] in R or x = b1 )
let y be set ; ::_thesis: ( not x in F1() or not y in F1() or not [x,y] in R or not [y,x] in R or x = y )
assume that
A29: x in F1() and
A30: y in F1() ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y )
reconsider x9 = x, y9 = y as Element of F1() by A29, A30;
assume that
A31: [x,y] in R and
A32: [y,x] in R ; ::_thesis: x = y
A33: P1[y9,x9] by A5, A32;
 P1[x9,y9] by A5, A31;
hence  x = y by A2, A33; ::_thesis: verum
end;
then  R partially_orders F1() by A15, A6, Def7;
then consider x being set  such that
A34: x is_minimal_in R by A14, A16, Th64;
take  x ; ::_thesis: ( x is Element of F1() & ( for y being Element of F1() st x <> y holds
not P1[y,x] ) )
thus  x is Element of F1() by A14, A34, Def12; ::_thesis: for y being Element of F1() st x <> y holds
not P1[y,x]
let y be Element of F1(); ::_thesis: ( x <> y implies not P1[y,x] )
assume  x <> y ; ::_thesis: P1[y,x]
then A35: not [y,x] in R by A14, A34, Def12;
 x in F1() by A14, A34, Def12;
hence  P1[y,x] by A5, A35; ::_thesis: verum
end;

theorem :: ORDERS_1:69
for R being Relation
for X being set st R partially_orders X & field R = X holds
ex P being Relation st
( R c= P & P linearly_orders X & field P = X )
proof
let R be Relation; ::_thesis: for X being set st R partially_orders X & field R = X holds
ex P being Relation st
( R c= P & P linearly_orders X & field P = X )
let X be set ; ::_thesis: ( R partially_orders X & field R = X implies ex P being Relation st
( R c= P & P linearly_orders X & field P = X ) )
assume that
A1: R partially_orders X and
A2: field R = X ; ::_thesis: ex P being Relation st
( R c= P & P linearly_orders X & field P = X )
defpred S1[ set ] means  ex P being Relation st
( $1 = P & R c= P & P partially_orders X & field P = X );
consider Rel being set  such that
A3: for x being set holds
( x in Rel iff ( x in bool [:X,X:] & S1[x] ) ) from XBOOLE_0:sch_1();
A4: for Z being set st Z <> {} & Z c= Rel & Z is c=-linear holds
union Z in Rel
proof
reconsider T = [:X,X:] as Relation ;
let Z be set ; ::_thesis: ( Z <> {} & Z c= Rel & Z is c=-linear implies union Z in Rel )
assume that
A5: Z <> {} and
A6: Z c= Rel and
A7: Z is c=-linear ; ::_thesis: union Z in Rel
A8: union (bool [:X,X:]) = T by ZFMISC_1:81;
 Z c= bool [:X,X:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in bool [:X,X:] )
assume  x in Z ; ::_thesis: x in bool [:X,X:]
hence  x in bool [:X,X:] by A3, A6; ::_thesis: verum
end;
then A9: union Z c= union (bool [:X,X:]) by ZFMISC_1:77;
then reconsider S = union Z as Relation ;
set y = the Element of Z;
 the Element of Z in Rel by A5, A6, TARSKI:def_3;
then consider P being Relation such that
A10: the Element of Z = P and
A11: R c= P and
A12: P partially_orders X and
 field P = X by A3;
A13: S is_antisymmetric_in X
proof
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or not [x,b1] in S or not [b1,x] in S or x = b1 )
let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in S or not [y,x] in S or x = y )
assume that
A14: x in X and
A15: y in X and
A16: [x,y] in S and
A17: [y,x] in S ; ::_thesis: x = y
consider X1 being set  such that
A18: [x,y] in X1 and
A19: X1 in Z by A16, TARSKI:def_4;
consider P1 being Relation such that
A20: X1 = P1 and
 R c= P1 and
A21: P1 partially_orders X and
 field P1 = X by A3, A6, A19;
consider X2 being set  such that
A22: [y,x] in X2 and
A23: X2 in Z by A17, TARSKI:def_4;
 X1,X2 are_c=-comparable by A7, A19, A23, ORDINAL1:def_8;
then A24: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9;
consider P2 being Relation such that
A25: X2 = P2 and
 R c= P2 and
A26: P2 partially_orders X and
 field P2 = X by A3, A6, A23;
A27: P2 is_antisymmetric_in X by A26, Def7;
 P1 is_antisymmetric_in X by A21, Def7;
hence  x = y by A14, A15, A18, A22, A24, A20, A25, A27, RELAT_2:def_4; ::_thesis: verum
end;
A28: S is_transitive_in X
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in X or not b1 in X or not b2 in X or not [x,b1] in S or not [b1,b2] in S or [x,b2] in S )
let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in S or not [y,z] in S or [x,z] in S )
assume that
A29: x in X and
A30: y in X and
A31: z in X and
A32: [x,y] in S and
A33: [y,z] in S ; ::_thesis: [x,z] in S
consider X1 being set  such that
A34: [x,y] in X1 and
A35: X1 in Z by A32, TARSKI:def_4;
consider P1 being Relation such that
A36: X1 = P1 and
 R c= P1 and
A37: P1 partially_orders X and
 field P1 = X by A3, A6, A35;
consider X2 being set  such that
A38: [y,z] in X2 and
A39: X2 in Z by A33, TARSKI:def_4;
 X1,X2 are_c=-comparable by A7, A35, A39, ORDINAL1:def_8;
then A40: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9;
consider P2 being Relation such that
A41: X2 = P2 and
 R c= P2 and
A42: P2 partially_orders X and
 field P2 = X by A3, A6, A39;
A43: P2 is_transitive_in X by A42, Def7;
 P1 is_transitive_in X by A37, Def7;
then  ( [x,z] in P1 or [x,z] in P2 ) by A29, A30, A31, A34, A38, A40, A36, A41, A43, RELAT_2:def_8;
hence  [x,z] in S by A35, A39, A36, A41, TARSKI:def_4; ::_thesis: verum
end;
A44: P is_reflexive_in X by A12, Def7;
 S is_reflexive_in X
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in S )
assume  x in X ; ::_thesis: [x,x] in S
then  [x,x] in P by A44, RELAT_2:def_1;
hence  [x,x] in S by A5, A10, TARSKI:def_4; ::_thesis: verum
end;
then A45: S partially_orders X by A28, A13, Def7;
A46: field S c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field S or x in X )
A47: now__::_thesis:_(_x_in_dom_S_&_x_in_field_S_implies_x_in_X_)
assume  x in dom S ; ::_thesis: ( not x in field S or x in X )
then consider y being set  such that
A48: [x,y] in S by XTUPLE_0:def_12;
consider Y being set  such that
A49: [x,y] in Y and
A50: Y in Z by A48, TARSKI:def_4;
 ex P being Relation st
( Y = P & R c= P & P partially_orders X & field P = X ) by A3, A6, A50;
hence  ( not x in field S or x in X ) by A49, RELAT_1:15; ::_thesis: verum
end;
A51: now__::_thesis:_(_x_in_rng_S_&_x_in_field_S_implies_x_in_X_)
assume  x in rng S ; ::_thesis: ( not x in field S or x in X )
then consider y being set  such that
A52: [y,x] in S by XTUPLE_0:def_13;
consider Y being set  such that
A53: [y,x] in Y and
A54: Y in Z by A52, TARSKI:def_4;
 ex P being Relation st
( Y = P & R c= P & P partially_orders X & field P = X ) by A3, A6, A54;
hence  ( not x in field S or x in X ) by A53, RELAT_1:15; ::_thesis: verum
end;
assume  x in field S ; ::_thesis: x in X
hence  x in X by A47, A51, XBOOLE_0:def_3; ::_thesis: verum
end;
A55: R c= S
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in R or [x,b1] in S )
let y be set ; ::_thesis: ( not [x,y] in R or [x,y] in S )
assume  [x,y] in R ; ::_thesis: [x,y] in S
hence  [x,y] in S by A5, A10, A11, TARSKI:def_4; ::_thesis: verum
end;
then  X c= field S by A2, RELAT_1:16;
then  field S = X by A46, XBOOLE_0:def_10;
hence  union Z in Rel by A3, A9, A8, A55, A45; ::_thesis: verum
end;
 R c= [:X,X:] by A2, Lm4;
then  Rel <> {} by A1, A2, A3;
then consider Y being set  such that
A56: Y in Rel and
A57: for Z being set st Z in Rel & Z <> Y holds
not Y c= Z by A4, Th67;
consider P being Relation such that
A58: Y = P and
A59: R c= P and
A60: P partially_orders X and
A61: field P = X by A3, A56;
take  P ; ::_thesis: ( R c= P & P linearly_orders X & field P = X )
thus  R c= P by A59; ::_thesis: ( P linearly_orders X & field P = X )
thus A62: ( P is_reflexive_in X & P is_transitive_in X & P is_antisymmetric_in X ) by A60, Def7; :: according to ORDERS_1:def_8 ::_thesis: ( P is_connected_in X & field P = X )
thus  P is_connected_in X ::_thesis: field P = X
proof
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or x = b1 or [x,b1] in P or [b1,x] in P )
let y be set ; ::_thesis: ( not x in X or not y in X or x = y or [x,y] in P or [y,x] in P )
assume that
A63: x in X and
A64: y in X and
 x <> y and
A65: not [x,y] in P and
A66: not [y,x] in P ; ::_thesis: contradiction
defpred S2[ set , set ] means ( [$1,$2] in P or ( [$1,x] in P & [y,$2] in P ) );
consider Q being Relation such that
A67: for z, u being set holds
( [z,u] in Q iff ( z in X & u in X & S2[z,u] ) ) from RELAT_1:sch_1();
A68: field Q c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in field Q or z in X )
A69: now__::_thesis:_(_z_in_dom_Q_&_z_in_field_Q_implies_z_in_X_)
assume  z in dom Q ; ::_thesis: ( not z in field Q or z in X )
then  ex u being set st [z,u] in Q by XTUPLE_0:def_12;
hence  ( not z in field Q or z in X ) by A67; ::_thesis: verum
end;
A70: now__::_thesis:_(_z_in_rng_Q_&_z_in_field_Q_implies_z_in_X_)
assume  z in rng Q ; ::_thesis: ( not z in field Q or z in X )
then  ex u being set st [u,z] in Q by XTUPLE_0:def_13;
hence  ( not z in field Q or z in X ) by A67; ::_thesis: verum
end;
assume  z in field Q ; ::_thesis: z in X
hence  z in X by A69, A70, XBOOLE_0:def_3; ::_thesis: verum
end;
A71: P c= Q
proof
let z be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [z,b1] in P or [z,b1] in Q )
let u be set ; ::_thesis: ( not [z,u] in P or [z,u] in Q )
assume A72: [z,u] in P ; ::_thesis: [z,u] in Q
then A73: u in field P by RELAT_1:15;
 z in field P by A72, RELAT_1:15;
hence  [z,u] in Q by A61, A67, A72, A73; ::_thesis: verum
end;
then  X c= field Q by A61, RELAT_1:16;
then A74: field Q = X by A68, XBOOLE_0:def_10;
A75: Q is_transitive_in X
proof
let a, b, c be set ; :: according to RELAT_2:def_8 ::_thesis: ( not a in X or not b in X or not c in X or not [a,b] in Q or not [b,c] in Q or [a,c] in Q )
assume that
A76: a in X and
A77: b in X and
A78: c in X and
A79: [a,b] in Q and
A80: [b,c] in Q ; ::_thesis: [a,c] in Q
A81: ( [b,c] in P or ( [b,x] in P & [y,c] in P ) ) by A67, A80;
 ( [a,b] in P or ( [a,x] in P & [y,b] in P ) ) by A67, A79;
then  ( [a,c] in P or ( [a,x] in P & [y,c] in P ) or ( [a,x] in P & [y,c] in P ) or [y,x] in P ) by A62, A63, A64, A76, A77, A78, A81, RELAT_2:def_8;
hence  [a,c] in Q by A66, A67, A76, A78; ::_thesis: verum
end;
A82: Q is_antisymmetric_in X
proof
let a, b be set ; :: according to RELAT_2:def_4 ::_thesis: ( not a in X or not b in X or not [a,b] in Q or not [b,a] in Q or a = b )
assume that
A83: a in X and
A84: b in X and
A85: [a,b] in Q and
A86: [b,a] in Q ; ::_thesis: a = b
A87: ( [b,a] in P or ( [b,x] in P & [y,a] in P ) ) by A67, A86;
 ( [a,b] in P or ( [a,x] in P & [y,b] in P ) ) by A67, A85;
then  ( a = b or ( [a,x] in P & [y,a] in P ) or [y,x] in P ) by A62, A63, A64, A83, A84, A87, RELAT_2:def_4, RELAT_2:def_8;
hence  a = b by A62, A63, A64, A66, A83, RELAT_2:def_8; ::_thesis: verum
end;
 Q is_reflexive_in X
proof
let z be set ; :: according to RELAT_2:def_1 ::_thesis: ( not z in X or [z,z] in Q )
assume A88: z in X ; ::_thesis: [z,z] in Q
then  [z,z] in P by A62, RELAT_2:def_1;
hence  [z,z] in Q by A67, A88; ::_thesis: verum
end;
then A89: Q partially_orders X by A75, A82, Def7;
A90: Q c= [:X,X:]
proof
let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [y,b1] in Q or [y,b1] in [:X,X:] )
let z be set ; ::_thesis: ( not [y,z] in Q or [y,z] in [:X,X:] )
assume A91: [y,z] in Q ; ::_thesis: [y,z] in [:X,X:]
then A92: z in X by A67;
 y in X by A67, A91;
hence  [y,z] in [:X,X:] by A92, ZFMISC_1:87; ::_thesis: verum
end;
 R c= Q by A59, A71, XBOOLE_1:1;
then  Q in Rel by A3, A90, A74, A89;
then A93: Q = P by A57, A58, A71;
A94: [y,y] in P by A62, A64, RELAT_2:def_1;
 [x,x] in P by A62, A63, RELAT_2:def_1;
hence  contradiction by A63, A64, A65, A67, A93, A94; ::_thesis: verum
end;
thus  field P = X by A61; ::_thesis: verum
end;

theorem :: ORDERS_1:70
for R being Relation holds R c= [:(field R),(field R):] by Lm4;

theorem :: ORDERS_1:71
for R being Relation
for X being set st R is reflexive & X c= field R holds
field (R |_2 X) = X by Lm5;

theorem :: ORDERS_1:72
for R being Relation
for X being set st R is_reflexive_in X holds
R |_2 X is reflexive by Lm6;

theorem :: ORDERS_1:73
for R being Relation
for X being set st R is_transitive_in X holds
R |_2 X is transitive by Lm7;

theorem :: ORDERS_1:74
for R being Relation
for X being set st R is_antisymmetric_in X holds
R |_2 X is antisymmetric by Lm8;

theorem :: ORDERS_1:75
for R being Relation
for X being set st R is_connected_in X holds
R |_2 X is connected by Lm9;

theorem :: ORDERS_1:76
for R being Relation
for X, Y being set st R is_connected_in X & Y c= X holds
R is_connected_in Y by Lm10;

theorem :: ORDERS_1:77
for R being Relation
for X, Y being set st R well_orders X & Y c= X holds
R well_orders Y by Lm17;

theorem :: ORDERS_1:78
for R being Relation st R is connected holds
R ~ is connected by Lm3;

theorem :: ORDERS_1:79
for R being Relation
for X being set st R is_reflexive_in X holds
R ~ is_reflexive_in X by Lm11;

theorem :: ORDERS_1:80
for R being Relation
for X being set st R is_transitive_in X holds
R ~ is_transitive_in X by Lm12;

theorem :: ORDERS_1:81
for R being Relation
for X being set st R is_antisymmetric_in X holds
R ~ is_antisymmetric_in X by Lm13;

theorem :: ORDERS_1:82
for R being Relation
for X being set st R is_connected_in X holds
R ~ is_connected_in X by Lm14;

theorem :: ORDERS_1:83
for R being Relation
for X being set holds (R |_2 X) ~ = (R ~) |_2 X by Lm15;

theorem :: ORDERS_1:84
for R being Relation holds R |_2 {} = {} by Lm16;

begin

theorem :: ORDERS_1:85
for f being Function
for Z being set st Z is finite & Z c= rng f holds
ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )
proof
let f be Function; ::_thesis: for Z being set st Z is finite & Z c= rng f holds
ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )
let Z be set ; ::_thesis: ( Z is finite & Z c= rng f implies ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z ) )
assume that
A1: Z is finite and
A2: Z c= rng f ; ::_thesis: ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )
percases ( Z = {} or Z <> {} ) ;
supposeA3: Z = {} ; ::_thesis: ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )
take Y = {} ; ::_thesis: ( Y c= dom f & Y is finite & f .: Y = Z )
thus  ( Y c= dom f & Y is finite ) by XBOOLE_1:2; ::_thesis: f .: Y = Z
thus  f .: Y = Z by A3; ::_thesis: verum
end;
supposeA4: Z <> {} ; ::_thesis: ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )
deffunc H1( set ) ->  set = f " {$1};
consider g being Function such that
A5: dom g = Z and
A6: for x being set st x in Z holds
g . x = H1(x) from FUNCT_1:sch_3();
reconsider AA = rng g as non empty set by A4, A5, RELAT_1:42;
set ff = the Choice_Function of AA;
take Y = the Choice_Function of AA .: AA; ::_thesis: ( Y c= dom f & Y is finite & f .: Y = Z )
A7: for X being set st X in AA holds
X <> {}
proof
let X be set ; ::_thesis: ( X in AA implies X <> {} )
assume  X in AA ; ::_thesis: X <> {}
then consider x being set  such that
A8: x in dom g and
A9: g . x = X by FUNCT_1:def_3;
 g . x = f " {x} by A5, A6, A8;
hence  X <> {} by A2, A5, A8, A9, FUNCT_1:72; ::_thesis: verum
end;
then A10: not {} in AA ;
thus A11: Y c= dom f ::_thesis: ( Y is finite & f .: Y = Z )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in dom f )
assume  x in Y ; ::_thesis: x in dom f
then consider y being set  such that
 y in dom the Choice_Function of AA and
A12: y in AA and
A13: the Choice_Function of AA . y = x by FUNCT_1:def_6;
 y in g .: Z by A5, A12, RELAT_1:113;
then consider z being set  such that
 z in dom g and
A14: z in Z and
A15: g . z = y by FUNCT_1:def_6;
A16: g . z = f " {z} by A6, A14;
 x in g . z by A10, A12, A13, A15, Def1;
hence  x in dom f by A16, FUNCT_1:def_7; ::_thesis: verum
end;
 AA = g .: Z by A5, RELAT_1:113;
hence  Y is finite by A1; ::_thesis: f .: Y = Z
set z = the Element of AA;
set y = the Element of the Element of AA;
 the Element of AA <> {} by A7;
then  the Element of the Element of AA in the Element of AA ;
then reconsider AA9 = union AA as non empty set by TARSKI:def_4;
reconsider f9 = the Choice_Function of AA as Function of AA,AA9 ;
A17: dom f9 = AA by FUNCT_2:def_1;
 for x being set holds
( x in f .: Y iff x in Z )
proof
let x be set ; ::_thesis: ( x in f .: Y iff x in Z )
thus  ( x in f .: Y implies x in Z ) ::_thesis: ( x in Z implies x in f .: Y )
proof
assume  x in f .: Y ; ::_thesis: x in Z
then consider y being set  such that
 y in dom f and
A18: y in Y and
A19: f . y = x by FUNCT_1:def_6;
consider z being set  such that
A20: z in dom the Choice_Function of AA and
 z in AA and
A21: the Choice_Function of AA . z = y by A18, FUNCT_1:def_6;
consider a being set  such that
A22: a in dom g and
A23: g . a = z by A20, FUNCT_1:def_3;
 g . a = f " {a} by A5, A6, A22;
then  y in f " {a} by A10, A20, A21, A23, Def1;
then  f . y in {a} by FUNCT_1:def_7;
hence  x in Z by A5, A19, A22, TARSKI:def_1; ::_thesis: verum
end;
set y = the Choice_Function of AA . (g . x);
assume A24: x in Z ; ::_thesis: x in f .: Y
then A25: g . x in AA by A5, FUNCT_1:def_3;
 g . x = f " {x} by A6, A24;
then  the Choice_Function of AA . (g . x) in f " {x} by A10, A25, Def1;
then  f . ( the Choice_Function of AA . (g . x)) in {x} by FUNCT_1:def_7;
then A26: f . ( the Choice_Function of AA . (g . x)) = x by TARSKI:def_1;
 the Choice_Function of AA . (g . x) in rng the Choice_Function of AA by A17, A25, FUNCT_1:def_3;
then  the Choice_Function of AA . (g . x) in Y by A17, RELAT_1:113;
hence  x in f .: Y by A11, A26, FUNCT_1:def_6; ::_thesis: verum
end;
hence  f .: Y = Z by TARSKI:1; ::_thesis: verum
end;
end;
end;

theorem Th86: :: ORDERS_1:86
for R being Relation st field R is finite holds
R is finite
proof
let R be Relation; ::_thesis: ( field R is finite implies R is finite )
assume  field R is finite ; ::_thesis: R is finite
then reconsider A = field R as finite set ;
 R c= [:A,A:] by Lm4;
hence  R is finite ; ::_thesis: verum
end;

theorem :: ORDERS_1:87
for R being Relation st dom R is finite & rng R is finite holds
R is finite
proof
let R be Relation; ::_thesis: ( dom R is finite & rng R is finite implies R is finite )
assume that
A1: dom R is finite and
A2: rng R is finite ; ::_thesis: R is finite
 field R is finite by A1, A2;
hence  R is finite by Th86; ::_thesis: verum
end;

registration
cluster order_type_of {} ->  empty ;
coherence
 order_type_of {} is empty
proof
 {} , RelIncl {} are_isomorphic by WELLORD1:38;
hence  order_type_of {} is empty by WELLORD2:def_2; ::_thesis: verum
end;
end;

theorem :: ORDERS_1:88
for O being Ordinal holds order_type_of (RelIncl O) = O
proof
let O be Ordinal; ::_thesis: order_type_of (RelIncl O) = O
 ( RelIncl O is well-ordering & RelIncl O, RelIncl O are_isomorphic ) by WELLORD1:38;
hence  order_type_of (RelIncl O) = O by WELLORD2:def_2; ::_thesis: verum
end;