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

begin

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

proof 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 b₁ being Function of M,(union M) st
for X being set st X in M holds
b₁ . X in X

proof end;

end;

:: deftheorem Def1 defines Choice_Function ORDERS_1:def 1 :
for M being non empty set st not {} in M holds
for b₂ being Function of M,(union M) holds
( b₂ is Choice_Function of M iff for X being set st X in M holds
b₂ . 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 end;

end;

theorem :: ORDERS_1:1

canceled;

theorem :: ORDERS_1:2

canceled;

theorem :: ORDERS_1:3

canceled;

theorem :: ORDERS_1:4

for D being non empty set holds not {} in BOOL D

proof end;

theorem :: ORDERS_1:5

for X being set
for D being non empty set holds
( D c= X iff D in BOOL X )

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

theorem :: ORDERS_1:6

canceled;

theorem :: ORDERS_1:7

canceled;

theorem :: ORDERS_1:8

canceled;

theorem :: ORDERS_1:9

canceled;

theorem :: ORDERS_1:10

canceled;

theorem :: ORDERS_1:11

canceled;

theorem Th12: :: ORDERS_1:12

for X, x being set
for O being Order of X st x in X holds
[x,x] in O

proof end;

theorem :: ORDERS_1:13

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

theorem :: ORDERS_1:14

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

theorem :: ORDERS_1:15

canceled;

theorem :: ORDERS_1:16

canceled;

theorem :: ORDERS_1:17

canceled;

theorem :: ORDERS_1:18

canceled;

theorem :: ORDERS_1:19

canceled;

theorem :: ORDERS_1:20

canceled;

theorem :: ORDERS_1:21

canceled;

theorem :: ORDERS_1:22

canceled;

theorem :: ORDERS_1:23

canceled;

theorem :: ORDERS_1:24

canceled;

theorem :: ORDERS_1:25

canceled;

theorem :: ORDERS_1:26

canceled;

theorem :: ORDERS_1:27

canceled;

theorem :: ORDERS_1:28

canceled;

theorem :: ORDERS_1:29

canceled;

theorem :: ORDERS_1:30

canceled;

theorem :: ORDERS_1:31

canceled;

theorem :: ORDERS_1:32

canceled;

theorem :: ORDERS_1:33

canceled;

theorem :: ORDERS_1:34

canceled;

theorem :: ORDERS_1:35

canceled;

theorem :: ORDERS_1:36

canceled;

theorem :: ORDERS_1:37

canceled;

theorem :: ORDERS_1:38

canceled;

theorem :: ORDERS_1:39

canceled;

theorem :: ORDERS_1:40

canceled;

theorem :: ORDERS_1:41

canceled;

theorem :: ORDERS_1:42

canceled;

theorem :: ORDERS_1:43

canceled;

theorem :: ORDERS_1:44

canceled;

theorem :: ORDERS_1:45

canceled;

theorem :: ORDERS_1:46

canceled;

theorem :: ORDERS_1:47

canceled;

theorem :: ORDERS_1:48

canceled;

theorem :: ORDERS_1:49

canceled;

theorem :: ORDERS_1:50

canceled;

theorem :: ORDERS_1:51

canceled;

theorem :: ORDERS_1:52

canceled;

theorem :: ORDERS_1:53

canceled;

theorem :: ORDERS_1:54

canceled;

theorem :: ORDERS_1:55

canceled;

theorem :: ORDERS_1:56

canceled;

theorem :: ORDERS_1:57

canceled;

theorem :: ORDERS_1:58

canceled;

theorem :: ORDERS_1:59

canceled;

theorem :: ORDERS_1:60

canceled;

theorem :: ORDERS_1:61

canceled;

theorem :: ORDERS_1:62

canceled;

theorem :: ORDERS_1:63

canceled;

theorem :: ORDERS_1:64

canceled;

theorem :: ORDERS_1:65

canceled;

theorem :: ORDERS_1:66

canceled;

theorem :: ORDERS_1:67

canceled;

theorem :: ORDERS_1:68

canceled;

theorem :: ORDERS_1:69

canceled;

theorem :: ORDERS_1:70

canceled;

theorem :: ORDERS_1:71

canceled;

theorem :: ORDERS_1:72

canceled;

theorem :: ORDERS_1:73

canceled;

theorem :: ORDERS_1:74

canceled;

theorem :: ORDERS_1:75

canceled;

theorem :: ORDERS_1:76

canceled;

theorem :: ORDERS_1:77

canceled;

theorem :: ORDERS_1:78

canceled;

theorem :: ORDERS_1:79

canceled;

theorem :: ORDERS_1:80

canceled;

theorem :: ORDERS_1:81

canceled;

theorem :: ORDERS_1:82

canceled;

theorem :: ORDERS_1:83

canceled;

theorem :: ORDERS_1:84

canceled;

theorem :: ORDERS_1:85

canceled;

theorem :: ORDERS_1:86

canceled;

theorem :: ORDERS_1:87

canceled;

theorem :: ORDERS_1:88

canceled;

theorem :: ORDERS_1:89

canceled;

theorem :: ORDERS_1:90

canceled;

theorem :: ORDERS_1:91

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

theorem :: ORDERS_1:92

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

theorem Th93: :: ORDERS_1:93

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

theorem Th94: :: ORDERS_1:94

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

theorem Th95: :: ORDERS_1:95

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

theorem :: ORDERS_1:96

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

theorem :: ORDERS_1:97

for X being set
for R being total Relation of X holds field R = X by Lm2;

theorem Th98: :: ORDERS_1:98

for A being set
for R being Relation of A st R is_reflexive_in A holds
( dom R = A & field R = A )

proof end;

begin

theorem Th99: :: ORDERS_1:99

for X being set
for O being Order of X holds
( dom O = X & rng O = X )

proof end;

theorem :: ORDERS_1:100

for X being set
for O being Order of X holds field O = X

proof end;

definition

let R be Relation;
attr R is being_quasi-order means :: ORDERS_1:def 3
( R is reflexive & R is transitive );
attr R is being_partial-order means :Def4: :: ORDERS_1:def 4
( R is reflexive & R is transitive & R is antisymmetric );
attr R 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:101

canceled;

theorem :: ORDERS_1:102

canceled;

theorem :: ORDERS_1:103

canceled;

theorem :: ORDERS_1:104

for R being Relation st R is being_quasi-order holds
R ~ is being_quasi-order

proof end;

theorem :: ORDERS_1:105

for R being Relation st R is being_partial-order holds
R ~ is being_partial-order

proof end;

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

proof end;

theorem Th106: :: ORDERS_1:106

for R being Relation st R is being_linear-order holds
R ~ is being_linear-order

proof end;

theorem :: ORDERS_1:107

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

theorem :: ORDERS_1:108

for R being Relation st R is being_linear-order holds
( R is being_quasi-order & R is being_partial-order )

proof end;

theorem Th109: :: ORDERS_1:109

for R being Relation st R is being_partial-order holds
R is being_quasi-order

proof end;

theorem :: ORDERS_1:110

for X being set
for O being Order of X holds O is being_partial-order by Def4;

theorem :: ORDERS_1:111

for X being set
for O being Order of X holds O is being_quasi-order

proof end;

theorem :: ORDERS_1:112

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

theorem :: ORDERS_1:113

for R being Relation
for X being set st R is being_quasi-order holds
R |_2 X is being_quasi-order

proof end;

theorem :: ORDERS_1:114

for R being Relation
for X being set st R is being_partial-order holds
R |_2 X is being_partial-order

proof end;

theorem :: ORDERS_1:115

for R being Relation
for X being set st R is being_linear-order holds
R |_2 X is being_linear-order

proof 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 set ;
coherence
for b₁ being Relation st b₁ is empty holds
( b₁ is being_quasi-order & b₁ is being_partial-order & b₁ is being_linear-order & b₁ is well-ordering )

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

end;

definition

let R be Relation;
let X be set ;
pred R quasi_orders X means :Def6: :: ORDERS_1:def 6
( R is_reflexive_in X & R is_transitive_in X );
pred R partially_orders X means :Def7: :: ORDERS_1:def 7
( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X );
pred R 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 :: ORDERS_1:116

canceled;

theorem :: ORDERS_1:117

canceled;

theorem :: ORDERS_1:118

canceled;

theorem :: ORDERS_1:119

canceled;

theorem :: ORDERS_1:120

canceled;

theorem :: ORDERS_1:121

canceled;

theorem :: ORDERS_1:122

canceled;

theorem :: ORDERS_1:123

canceled;

theorem Th124: :: ORDERS_1:124

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

theorem Th125: :: ORDERS_1:125

for R being Relation
for X being set st R linearly_orders X holds
( R quasi_orders X & R partially_orders X )

proof end;

theorem :: ORDERS_1:126

for R being Relation
for X being set st R partially_orders X holds
R quasi_orders X

proof end;

theorem Th127: :: ORDERS_1:127

for R being Relation st R is being_quasi-order holds
R quasi_orders field R

proof end;

theorem :: ORDERS_1:128

for R being Relation
for Y, X being set st R quasi_orders Y & X c= Y holds
R quasi_orders X

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem :: ORDERS_1:129

for R being Relation
for X being set st R quasi_orders X holds
R |_2 X is being_quasi-order

proof end;

theorem Th130: :: ORDERS_1:130

for R being Relation st R is being_partial-order holds
R partially_orders field R

proof end;

theorem :: ORDERS_1:131

for R being Relation
for Y, X being set st R partially_orders Y & X c= Y holds
R partially_orders X

proof end;

theorem :: ORDERS_1:132

for R being Relation
for X being set st R partially_orders X holds
R |_2 X is being_partial-order

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

theorem :: ORDERS_1:133

for R being Relation st R is being_linear-order holds
R linearly_orders field R

proof end;

theorem :: ORDERS_1:134

for R being Relation
for Y, X being set st R linearly_orders Y & X c= Y holds
R linearly_orders X

proof end;

theorem :: ORDERS_1:135

for R being Relation
for X being set st R linearly_orders X holds
R |_2 X is being_linear-order

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem :: ORDERS_1:136

for R being Relation
for X being set st R quasi_orders X holds
R ~ quasi_orders X

proof end;

theorem Th137: :: ORDERS_1:137

for R being Relation
for X being set st R partially_orders X holds
R ~ partially_orders X

proof end;

theorem :: ORDERS_1:138

for R being Relation
for X being set st R linearly_orders X holds
R ~ linearly_orders X

proof end;

theorem :: ORDERS_1:139

for X being set
for O being Order of X holds O quasi_orders X

proof end;

theorem :: ORDERS_1:140

for X being set
for O being Order of X holds O partially_orders X

proof end;

theorem Th141: :: ORDERS_1:141

for R being Relation
for X being set st R partially_orders X holds
R |_2 X is Order of X

proof end;

theorem :: ORDERS_1:142

for R being Relation
for X being set st R linearly_orders X holds
R |_2 X is Order of X by Th125, Th141;

theorem :: ORDERS_1:143

for R being Relation
for X being set st R well_orders X holds
R |_2 X is Order of X by Th124, Th141;

theorem :: ORDERS_1:144

canceled;

theorem :: ORDERS_1:145

canceled;

theorem :: ORDERS_1:146

for X being set holds
( id X quasi_orders X & id X partially_orders X )

proof end;

definition

let R be Relation;
let X be set ;
pred X 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 ) );
pred X 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 end;

Lm16: now

let R be Relation; :: thesis: R |_2 {} = {}
thus R |_2 {} = ({} | R) | {} by WELLORD1:17
.= {} ; :: thesis: verum

end;

theorem :: ORDERS_1:147

canceled;

theorem :: ORDERS_1:148

canceled;

theorem Th149: :: ORDERS_1:149

for R being Relation
for X being set st X has_upper_Zorn_property_wrt R holds
X <> {}

proof end;

theorem :: ORDERS_1:150

for R being Relation
for X being set st X has_lower_Zorn_property_wrt R holds
X <> {}

proof end;

theorem Th151: :: ORDERS_1:151

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

theorem :: ORDERS_1:152

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

definition

let R be Relation;
let x be set ;
pred x 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 ) ) );
pred x 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 ) ) );
pred x 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 ) );
pred x 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:153

canceled;

theorem :: ORDERS_1:154

canceled;

theorem :: ORDERS_1:155

canceled;

theorem :: ORDERS_1:156

canceled;

theorem :: ORDERS_1:157

for R being Relation
for x being set st x is_inferior_of R & R is antisymmetric holds
x is_minimal_in R

proof end;

theorem :: ORDERS_1:158

for R being Relation
for x being set st x is_superior_of R & R is antisymmetric holds
x is_maximal_in R

proof end;

theorem :: ORDERS_1:159

for R being Relation
for x being set st x is_minimal_in R & R is connected holds
x is_inferior_of R

proof end;

theorem :: ORDERS_1:160

for R being Relation
for x being set st x is_maximal_in R & R is connected holds
x is_superior_of R

proof end;

theorem :: ORDERS_1:161

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

theorem :: ORDERS_1:162

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

theorem Th163: :: ORDERS_1:163

for R being Relation
for x being set holds
( x is_minimal_in R iff x is_maximal_in R ~ )

proof end;

theorem :: ORDERS_1:164

for R being Relation
for x being set holds
( x is_minimal_in R ~ iff x is_maximal_in R )

proof end;

theorem :: ORDERS_1:165

for R being Relation
for x being set holds
( x is_inferior_of R iff x is_superior_of R ~ )

proof end;

theorem :: ORDERS_1:166

for R being Relation
for x being set holds
( x is_inferior_of R ~ iff x is_superior_of R )

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

theorem :: ORDERS_1:167

canceled;

theorem :: ORDERS_1:168

canceled;

theorem :: ORDERS_1:169

canceled;

theorem :: ORDERS_1:170

canceled;

theorem :: ORDERS_1:171

canceled;

theorem :: ORDERS_1:172

canceled;

theorem Th173: :: ORDERS_1:173

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

theorem Th174: :: ORDERS_1:174

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

theorem Th175: :: ORDERS_1:175

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

theorem Th176: :: ORDERS_1:176

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

theorem Th177: :: ORDERS_1:177

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

theorem :: ORDERS_1:178

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

scheme :: ORDERS_1:sch 1
ZornMax{ F₁() -> non empty set , P₁[ set , set ] } :

ex x being Element of F₁() st
for y being Element of F₁() st x <> y holds
not P₁[x,y]

provided

A1: for x being Element of F₁() holds P₁[x,x] and
A2: for x, y being Element of F₁() st P₁[x,y] & P₁[y,x] holds
x = y and
A3: for x, y, z being Element of F₁() st P₁[x,y] & P₁[y,z] holds
P₁[x,z] and
A4: for X being set st X c= F₁() & ( for x, y being Element of F₁() st x in X & y in X & P₁[x,y] holds
P₁[y,x] ) holds
ex y being Element of F₁() st
for x being Element of F₁() st x in X holds
P₁[x,y]

proof end;

scheme :: ORDERS_1:sch 2
ZornMin{ F₁() -> non empty set , P₁[ set , set ] } :

ex x being Element of F₁() st
for y being Element of F₁() st x <> y holds
not P₁[y,x]

provided

A1: for x being Element of F₁() holds P₁[x,x] and
A2: for x, y being Element of F₁() st P₁[x,y] & P₁[y,x] holds
x = y and
A3: for x, y, z being Element of F₁() st P₁[x,y] & P₁[y,z] holds
P₁[x,z] and
A4: for X being set st X c= F₁() & ( for x, y being Element of F₁() st x in X & y in X & P₁[x,y] holds
P₁[y,x] ) holds
ex y being Element of F₁() st
for x being Element of F₁() st x in X holds
P₁[y,x]

proof end;

theorem :: ORDERS_1:179

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

theorem :: ORDERS_1:180

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

theorem :: ORDERS_1:181

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:182

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:183

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:184

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:185

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:186

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:187

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:188

for R being Relation st R is connected holds
R ~ is connected by Lm3;

theorem :: ORDERS_1:189

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:190

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:191

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:192

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:193

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

theorem :: ORDERS_1:194

for R being Relation holds R |_2 {} = {} by Lm16;

begin

theorem :: ORDERS_1:195

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

theorem Th196: :: ORDERS_1:196

for R being Relation st field R is finite holds
R is finite

proof end;

theorem :: ORDERS_1:197

for R being Relation st dom R is finite & rng R is finite holds
R is finite

proof end;

registration

cluster order_type_of {} -> empty ;
coherence
order_type_of {} is empty

proof end;

end;

theorem :: ORDERS_1:198

for O being Ordinal holds order_type_of (RelIncl O) = O

proof end;