:: Partially Ordered Sets
:: by Wojciech A. Trybulec
::
:: Received August 30, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

Lm1:  for Y being set holds
( ex X being set st
( X <> {} &amp; X in Y ) iff union Y <> {} )
proofend;

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
proofend;
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
proofend;
end;

theorem :: ORDERS_1:1
for D being non empty set holds not {} in BOOL D
proofend;

theorem :: ORDERS_1:2
for X being set
for D being non empty set holds
( D c= X iff D in BOOL X )
proofend;

::
:: Orders.
::
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
proofend;

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
proofend;

theorem :: ORDERS_1:4
for X, x, y being set
for O being Order of X st x in X &amp; y in X &amp; [x,y] in O &amp; [y,x] in O holds
x = y
proofend;

theorem :: ORDERS_1:5
for X, x, y, z being set
for O being Order of X st x in X &amp; y in X &amp; z in X &amp; [x,y] in O &amp; [y,z] in O holds
[x,z] in O
proofend;

theorem :: ORDERS_1:6
for Y being set holds
( ex X being set st
( X <> {} &amp; 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 &amp; P is_connected_in X ) )
proofend;

theorem Th8: :: ORDERS_1:8
for X, Y being set
for P being Relation st P is_reflexive_in X &amp; Y c= X holds
P is_reflexive_in Y
proofend;

theorem Th9: :: ORDERS_1:9
for X, Y being set
for P being Relation st P is_antisymmetric_in X &amp; Y c= X holds
P is_antisymmetric_in Y
proofend;

theorem Th10: :: ORDERS_1:10
for X, Y being set
for P being Relation st P is_transitive_in X &amp; Y c= X holds
P is_transitive_in Y
proofend;

theorem :: ORDERS_1:11
for X, Y being set
for P being Relation st P is_strongly_connected_in X &amp; Y c= X holds
P is_strongly_connected_in Y
proofend;

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 &amp; field R = A )
proofend;

begin

::
:: Orders.
::
theorem Th14: :: ORDERS_1:14
for X being set
for O being Order of X holds
( dom O = X &amp; rng O = X )
proofend;

theorem :: ORDERS_1:15
for X being set
for O being Order of X holds field O = X
proofend;

definition
let R be Relation;
attrR is being_quasi-order  means :: ORDERS_1:def 3
( R is reflexive &amp; R is transitive );
attrR is being_partial-order  means :Def4: :: ORDERS_1:def 4
( R is reflexive &amp; R is transitive &amp; R is antisymmetric );
attrR is being_linear-order  means :Def5: :: ORDERS_1:def 5
( R is reflexive &amp; R is transitive &amp; R is antisymmetric &amp; 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 &amp; 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 &amp; R is transitive &amp; 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 &amp; R is transitive &amp; R is antisymmetric &amp; R is connected ) );

theorem :: ORDERS_1:16
for R being Relation st R is being_quasi-order holds
R ~ is being_quasi-order
proofend;

theorem :: ORDERS_1:17
for R being Relation st R is being_partial-order holds
R ~ is being_partial-order
proofend;

Lm3:  for R being Relation st R is connected holds
R ~ is connected
proofend;

theorem Th18: :: ORDERS_1:18
for R being Relation st R is being_linear-order holds
R ~ is being_linear-order
proofend;

theorem :: ORDERS_1:19
for R being Relation st R is well-ordering holds
( R is being_quasi-order &amp; R is being_partial-order &amp; R is being_linear-order )
proofend;

theorem :: ORDERS_1:20
for R being Relation st R is being_linear-order holds
( R is being_quasi-order &amp; R is being_partial-order )
proofend;

theorem Th21: :: ORDERS_1:21
for R being Relation st R is being_partial-order holds
R is being_quasi-order
proofend;

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
proofend;

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):]
proofend;

Lm5:  for R being Relation
for X being set st R is reflexive &amp; X c= field R holds
field (R |_2 X) = X
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; b1 is being_partial-order &amp; b1 is being_linear-order &amp; b1 is well-ordering )
proofend;
end;

registration
let X be set ;
cluster id X ->  being_quasi-order being_partial-order ;
coherence
 ( id X is being_quasi-order &amp; id X is being_partial-order )
proofend;
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 &amp; R is_transitive_in X );
predR partially_orders X means :Def7: :: ORDERS_1:def 7
( R is_reflexive_in X &amp; R is_transitive_in X &amp; R is_antisymmetric_in X );
predR linearly_orders X means :: ORDERS_1:def 8
( R is_reflexive_in X &amp; R is_transitive_in X &amp; R is_antisymmetric_in X &amp; 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 &amp; 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 &amp; R is_transitive_in X &amp; 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 &amp; R is_transitive_in X &amp; R is_antisymmetric_in X &amp; 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 &amp; R partially_orders X &amp; R linearly_orders X )
proofend;

theorem Th29: :: ORDERS_1:29
for R being Relation
for X being set st R linearly_orders X holds
( R quasi_orders X &amp; R partially_orders X )
proofend;

theorem :: ORDERS_1:30
for R being Relation
for X being set st R partially_orders X holds
R quasi_orders X
proofend;

theorem Th31: :: ORDERS_1:31
for R being Relation st R is being_quasi-order holds
R quasi_orders field R
proofend;

theorem :: ORDERS_1:32
for R being Relation
for Y, X being set st R quasi_orders Y &amp; X c= Y holds
R quasi_orders X
proofend;

Lm6:  for R being Relation
for X being set st R is_reflexive_in X holds
R |_2 X is reflexive
proofend;

Lm7:  for R being Relation
for X being set st R is_transitive_in X holds
R |_2 X is transitive
proofend;

Lm8:  for R being Relation
for X being set st R is_antisymmetric_in X holds
R |_2 X is antisymmetric
proofend;

Lm9:  for R being Relation
for X being set st R is_connected_in X holds
R |_2 X is connected
proofend;

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
proofend;

theorem Th34: :: ORDERS_1:34
for R being Relation st R is being_partial-order holds
R partially_orders field R
proofend;

theorem :: ORDERS_1:35
for R being Relation
for Y, X being set st R partially_orders Y &amp; X c= Y holds
R partially_orders X
proofend;

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
proofend;

Lm10:  for R being Relation
for X, Y being set st R is_connected_in X &amp; Y c= X holds
R is_connected_in Y
proofend;

theorem :: ORDERS_1:37
for R being Relation st R is being_linear-order holds
R linearly_orders field R
proofend;

theorem :: ORDERS_1:38
for R being Relation
for Y, X being set st R linearly_orders Y &amp; X c= Y holds
R linearly_orders X
proofend;

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
proofend;

Lm11:  for R being Relation
for X being set st R is_reflexive_in X holds
R ~ is_reflexive_in X
proofend;

Lm12:  for R being Relation
for X being set st R is_transitive_in X holds
R ~ is_transitive_in X
proofend;

Lm13:  for R being Relation
for X being set st R is_antisymmetric_in X holds
R ~ is_antisymmetric_in X
proofend;

Lm14:  for R being Relation
for X being set st R is_connected_in X holds
R ~ is_connected_in X
proofend;

theorem :: ORDERS_1:40
for R being Relation
for X being set st R quasi_orders X holds
R ~ quasi_orders X
proofend;

theorem Th41: :: ORDERS_1:41
for R being Relation
for X being set st R partially_orders X holds
R ~ partially_orders X
proofend;

theorem :: ORDERS_1:42
for R being Relation
for X being set st R linearly_orders X holds
R ~ linearly_orders X
proofend;

theorem :: ORDERS_1:43
for X being set
for O being Order of X holds O quasi_orders X
proofend;

theorem :: ORDERS_1:44
for X being set
for O being Order of X holds O partially_orders X
proofend;

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
proofend;

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 &amp; id X partially_orders X )
proofend;

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 &amp; R |_2 Y is being_linear-order holds
ex x being set st
( x in X &amp; ( 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 &amp; R |_2 Y is being_linear-order holds
ex x being set st
( x in X &amp; ( 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 &amp; R |_2 Y is being_linear-order holds
ex x being set st
( x in X &amp; ( 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 &amp; R |_2 Y is being_linear-order holds
ex x being set st
( x in X &amp; ( 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
proofend;

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 <> {}
proofend;

theorem :: ORDERS_1:50
for R being Relation
for X being set st X has_lower_Zorn_property_wrt R holds
X <> {}
proofend;

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 ~ )
proofend;

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 )
proofend;

definition
let R be Relation;
let x be set ;
predx is_maximal_in R means :Def11: :: ORDERS_1:def 11
( x in field R &amp; ( 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 &amp; ( 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 &amp; ( for y being set st y in field R &amp; y <> x holds
[y,x] in R ) );
predx is_inferior_of R means :Def14: :: ORDERS_1:def 14
( x in field R &amp; ( for y being set st y in field R &amp; 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 &amp; ( 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 &amp; ( 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 &amp; ( for y being set st y in field R &amp; 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 &amp; ( for y being set st y in field R &amp; 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 &amp; R is antisymmetric holds
x is_minimal_in R
proofend;

theorem :: ORDERS_1:54
for R being Relation
for x being set st x is_superior_of R &amp; R is antisymmetric holds
x is_maximal_in R
proofend;

theorem :: ORDERS_1:55
for R being Relation
for x being set st x is_minimal_in R &amp; R is connected holds
x is_inferior_of R
proofend;

theorem :: ORDERS_1:56
for R being Relation
for x being set st x is_maximal_in R &amp; R is connected holds
x is_superior_of R
proofend;

theorem :: ORDERS_1:57
for R being Relation
for x, X being set st x in X &amp; x is_superior_of R &amp; X c= field R &amp; R is reflexive holds
X has_upper_Zorn_property_wrt R
proofend;

theorem :: ORDERS_1:58
for R being Relation
for x, X being set st x in X &amp; x is_inferior_of R &amp; X c= field R &amp; R is reflexive holds
X has_lower_Zorn_property_wrt R
proofend;

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 ~ )
proofend;

theorem :: ORDERS_1:60
for R being Relation
for x being set holds
( x is_minimal_in R ~ iff x is_maximal_in R )
proofend;

theorem :: ORDERS_1:61
for R being Relation
for x being set holds
( x is_inferior_of R iff x is_superior_of R ~ )
proofend;

theorem :: ORDERS_1:62
for R being Relation
for x being set holds
( x is_inferior_of R ~ iff x is_superior_of R )
proofend;

Lm17:  for R being Relation
for X, Y being set st R well_orders X &amp; Y c= X holds
R well_orders Y
proofend;

theorem Th63: :: ORDERS_1:63
for R being Relation
for X being set st R partially_orders X &amp; field R = X &amp; X has_upper_Zorn_property_wrt R holds
ex x being set st x is_maximal_in R
proofend;

theorem Th64: :: ORDERS_1:64
for R being Relation
for X being set st R partially_orders X &amp; field R = X &amp; X has_lower_Zorn_property_wrt R holds
ex x being set st x is_minimal_in R
proofend;

:: [WP: ] Kuratowski-Zorn_Lemma
:: [WP: ] Zorn_Lemma
theorem Th65: :: ORDERS_1:65
for X being set st X <> {} &amp; ( for Z being set st Z c= X &amp; Z is c=-linear holds
ex Y being set st
( Y in X &amp; ( for X1 being set st X1 in Z holds
X1 c= Y ) ) ) holds
ex Y being set st
( Y in X &amp; ( for Z being set st Z in X &amp; Z <> Y holds
not Y c= Z ) )
proofend;

theorem Th66: :: ORDERS_1:66
for X being set st X <> {} &amp; ( for Z being set st Z c= X &amp; Z is c=-linear holds
ex Y being set st
( Y in X &amp; ( for X1 being set st X1 in Z holds
Y c= X1 ) ) ) holds
ex Y being set st
( Y in X &amp; ( for Z being set st Z in X &amp; Z <> Y holds
not Z c= Y ) )
proofend;

theorem Th67: :: ORDERS_1:67
for X being set st X <> {} &amp; ( for Z being set st Z <> {} &amp; Z c= X &amp; Z is c=-linear holds
union Z in X ) holds
ex Y being set st
( Y in X &amp; ( for Z being set st Z in X &amp; Z <> Y holds
not Y c= Z ) )
proofend;

theorem :: ORDERS_1:68
for X being set st X <> {} &amp; ( for Z being set st Z <> {} &amp; Z c= X &amp; Z is c=-linear holds
meet Z in X ) holds
ex Y being set st
( Y in X &amp; ( for Z being set st Z in X &amp; Z <> Y holds
not Z c= Y ) )
proofend;

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] &amp; P1[y,x] holds
x = y and
A3: for x, y, z being Element of F1() st P1[x,y] &amp; P1[y,z] holds
P1[x,z] and
A4: for X being set st X c= F1() &amp; ( for x, y being Element of F1() st x in X &amp; y in X &amp; 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]
proofend;

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] &amp; P1[y,x] holds
x = y and
A3: for x, y, z being Element of F1() st P1[x,y] &amp; P1[y,z] holds
P1[x,z] and
A4: for X being set st X c= F1() &amp; ( for x, y being Element of F1() st x in X &amp; y in X &amp; 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]
proofend;

::
:: Orders - continuation.
::
theorem :: ORDERS_1:69
for R being Relation
for X being set st R partially_orders X &amp; field R = X holds
ex P being Relation st
( R c= P &amp; P linearly_orders X &amp; field P = X )
proofend;

::
:: Auxiliary theorems.
::
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 &amp; 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 &amp; 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 &amp; 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

:: from COMPTS_1
theorem :: ORDERS_1:85
for f being Function
for Z being set st Z is finite &amp; Z c= rng f holds
ex Y being set st
( Y c= dom f &amp; Y is finite &amp; f .: Y = Z )
proofend;

:: from AMISTD_3, 2006.03.26, A.T.
theorem Th86: :: ORDERS_1:86
for R being Relation st field R is finite holds
R is finite
proofend;

theorem :: ORDERS_1:87
for R being Relation st dom R is finite &amp; rng R is finite holds
R is finite
proofend;

:: from AMISTD_3, 2010.01.10, A.T
registration
cluster order_type_of {} ->  empty ;
coherence
 order_type_of {} is empty
proofend;
end;

theorem :: ORDERS_1:88
for O being Ordinal holds order_type_of (RelIncl O) = O
proofend;