:: Kuratowski - Zorn Lemma
:: by Wojciech A. Trybulec and Grzegorz Bancerek
::
:: Received September 19, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem ORDERS_2:def 1 :
canceled;
:: deftheorem ORDERS_2:def 2 :
canceled;
:: deftheorem Def3 defines total ORDERS_2:def 3 :
:: deftheorem Def4 defines reflexive ORDERS_2:def 4 :
:: deftheorem Def5 defines transitive ORDERS_2:def 5 :
:: deftheorem Def6 defines antisymmetric ORDERS_2:def 6 :
Lm1:
for x being set
for A being non empty Poset
for S being Subset of A st x in S holds
x is Element of A
;
:: deftheorem ORDERS_2:def 7 :
canceled;
:: deftheorem ORDERS_2:def 8 :
canceled;
:: deftheorem Def9 defines <= ORDERS_2:def 9 :
:: deftheorem Def10 defines < ORDERS_2:def 10 :
for
A being
RelStr for
a1,
a2 being
Element of
A holds
(
a1 < a2 iff (
a1 <= a2 &
a1 <> a2 ) );
theorem :: ORDERS_2:1
canceled;
theorem :: ORDERS_2:2
canceled;
theorem :: ORDERS_2:3
canceled;
theorem :: ORDERS_2:4
canceled;
theorem :: ORDERS_2:5
canceled;
theorem :: ORDERS_2:6
canceled;
theorem :: ORDERS_2:7
canceled;
theorem :: ORDERS_2:8
canceled;
theorem :: ORDERS_2:9
canceled;
theorem :: ORDERS_2:10
canceled;
theorem :: ORDERS_2:11
canceled;
theorem :: ORDERS_2:12
canceled;
theorem :: ORDERS_2:13
canceled;
theorem :: ORDERS_2:14
canceled;
theorem :: ORDERS_2:15
canceled;
theorem :: ORDERS_2:16
canceled;
theorem :: ORDERS_2:17
canceled;
theorem :: ORDERS_2:18
canceled;
theorem :: ORDERS_2:19
canceled;
theorem :: ORDERS_2:20
canceled;
theorem :: ORDERS_2:21
canceled;
theorem :: ORDERS_2:22
canceled;
theorem :: ORDERS_2:23
canceled;
theorem Th24: :: ORDERS_2:24
theorem Th25: :: ORDERS_2:25
theorem Th26: :: ORDERS_2:26
theorem :: ORDERS_2:27
canceled;
theorem Th28: :: ORDERS_2:28
theorem Th29: :: ORDERS_2:29
theorem Th30: :: ORDERS_2:30
theorem :: ORDERS_2:31
canceled;
theorem Th32: :: ORDERS_2:32
:: deftheorem Def11 defines strongly_connected ORDERS_2:def 11 :
theorem :: ORDERS_2:33
canceled;
theorem :: ORDERS_2:34
canceled;
theorem Th35: :: ORDERS_2:35
theorem Th36: :: ORDERS_2:36
theorem :: ORDERS_2:37
theorem Th38: :: ORDERS_2:38
theorem Th39: :: ORDERS_2:39
theorem Th40: :: ORDERS_2:40
:: deftheorem defines UpperCone ORDERS_2:def 12 :
:: deftheorem defines LowerCone ORDERS_2:def 13 :
theorem :: ORDERS_2:41
canceled;
theorem :: ORDERS_2:42
canceled;
theorem Th43: :: ORDERS_2:43
theorem :: ORDERS_2:44
theorem :: ORDERS_2:45
theorem :: ORDERS_2:46
theorem Th47: :: ORDERS_2:47
theorem :: ORDERS_2:48
theorem Th49: :: ORDERS_2:49
theorem Th50: :: ORDERS_2:50
theorem :: ORDERS_2:51
theorem Th52: :: ORDERS_2:52
:: deftheorem defines InitSegm ORDERS_2:def 14 :
:: deftheorem Def15 defines Initial_Segm ORDERS_2:def 15 :
theorem :: ORDERS_2:53
canceled;
theorem :: ORDERS_2:54
canceled;
theorem :: ORDERS_2:55
canceled;
theorem :: ORDERS_2:56
canceled;
theorem Th57: :: ORDERS_2:57
theorem :: ORDERS_2:58
canceled;
theorem :: ORDERS_2:59
canceled;
theorem :: ORDERS_2:60
theorem :: ORDERS_2:61
canceled;
theorem Th62: :: ORDERS_2:62
theorem :: ORDERS_2:63
canceled;
theorem :: ORDERS_2:64
theorem Th65: :: ORDERS_2:65
theorem :: ORDERS_2:66
canceled;
theorem Th67: :: ORDERS_2:67
theorem Th68: :: ORDERS_2:68
theorem Th69: :: ORDERS_2:69
theorem Th70: :: ORDERS_2:70
theorem Th71: :: ORDERS_2:71
theorem :: ORDERS_2:72
theorem Th73: :: ORDERS_2:73
:: deftheorem Def16 defines Chain ORDERS_2:def 16 :
theorem :: ORDERS_2:74
canceled;
theorem :: ORDERS_2:75
canceled;
theorem :: ORDERS_2:76
canceled;
theorem :: ORDERS_2:77
canceled;
theorem Th78: :: ORDERS_2:78
theorem Th79: :: ORDERS_2:79
theorem Th80: :: ORDERS_2:80
theorem :: ORDERS_2:81
theorem :: ORDERS_2:82
theorem Th83: :: ORDERS_2:83
theorem Th84: :: ORDERS_2:84
:: deftheorem Def17 defines Chains ORDERS_2:def 17 :
Lm2:
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Subset of A
Lm3:
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of A
theorem :: ORDERS_2:85
canceled;
theorem :: ORDERS_2:86
canceled;
theorem Th87: :: ORDERS_2:87
theorem Th88: :: ORDERS_2:88
theorem Th89: :: ORDERS_2:89
theorem :: ORDERS_2:90
canceled;
theorem :: ORDERS_2:91
canceled;
theorem :: ORDERS_2:92
canceled;
theorem :: ORDERS_2:93
canceled;
theorem :: ORDERS_2:94
canceled;
theorem :: ORDERS_2:95
canceled;
theorem :: ORDERS_2:96
canceled;
theorem :: ORDERS_2:97
canceled;
theorem :: ORDERS_2:98
canceled;
theorem :: ORDERS_2:99
canceled;
theorem :: ORDERS_2:100
canceled;
theorem :: ORDERS_2:101
canceled;
theorem :: ORDERS_2:102
canceled;
theorem :: ORDERS_2:103
canceled;
theorem :: ORDERS_2:104
canceled;
theorem :: ORDERS_2:105
canceled;
theorem :: ORDERS_2:106
canceled;
theorem Th107: :: ORDERS_2:107
theorem :: ORDERS_2:108
theorem :: ORDERS_2:109
theorem :: ORDERS_2:110
canceled;
theorem :: ORDERS_2:111
canceled;
theorem :: ORDERS_2:112
canceled;
theorem :: ORDERS_2:113
canceled;
theorem :: ORDERS_2:114
canceled;
theorem :: ORDERS_2:115
canceled;
theorem :: ORDERS_2:116
canceled;
theorem :: ORDERS_2:117
canceled;
theorem :: ORDERS_2:118
canceled;
theorem :: ORDERS_2:119
canceled;
theorem :: ORDERS_2:120
canceled;
theorem :: ORDERS_2:121
canceled;
theorem :: ORDERS_2:122
canceled;
theorem :: ORDERS_2:123
canceled;
theorem :: ORDERS_2:124
canceled;
theorem :: ORDERS_2:125
canceled;
theorem :: ORDERS_2:126
canceled;
theorem :: ORDERS_2:127
canceled;
theorem :: ORDERS_2:128
canceled;
theorem :: ORDERS_2:129
canceled;
theorem :: ORDERS_2:130
canceled;
theorem :: ORDERS_2:131
canceled;
theorem :: ORDERS_2:132
canceled;
theorem :: ORDERS_2:133
canceled;
theorem :: ORDERS_2:134
canceled;
theorem :: ORDERS_2:135
theorem :: ORDERS_2:136
theorem :: ORDERS_2:137
canceled;
theorem :: ORDERS_2:138
canceled;
theorem :: ORDERS_2:139
canceled;
theorem :: ORDERS_2:140
canceled;
theorem :: ORDERS_2:141
canceled;
theorem :: ORDERS_2:142
canceled;
theorem :: ORDERS_2:143
canceled;
theorem :: ORDERS_2:144
canceled;
theorem :: ORDERS_2:145
canceled;
theorem :: ORDERS_2:146
canceled;
theorem :: ORDERS_2:147
canceled;
theorem :: ORDERS_2:148
canceled;
theorem :: ORDERS_2:149
canceled;
theorem :: ORDERS_2:150
canceled;
theorem :: ORDERS_2:151
canceled;
theorem :: ORDERS_2:152
canceled;
theorem :: ORDERS_2:153
canceled;
theorem :: ORDERS_2:154
canceled;
theorem :: ORDERS_2:155
canceled;
theorem :: ORDERS_2:156
canceled;
theorem :: ORDERS_2:157
canceled;
theorem :: ORDERS_2:158
theorem :: ORDERS_2:159
theorem :: ORDERS_2:160
theorem :: ORDERS_2:161
Lm4:
for X, Y being set
for R being Relation st R is_connected_in X & Y c= X holds
R is_connected_in Y
Lm5:
for X, Y being set
for R being Relation st R well_orders X & Y c= X holds
R well_orders Y
theorem Th162: :: ORDERS_2:162
theorem :: ORDERS_2:163