begin
Lm1:
for Y being set holds
( ex X being set st
( X <> {} & X in Y ) iff union Y <> {} )
:: deftheorem Def1 defines Choice_Function ORDERS_1:def 1 :
:: deftheorem defines BOOL ORDERS_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
Lm2:
for X being set
for R being total Relation of holds field R = X
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th12:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th93:
theorem Th94:
theorem Th95:
theorem
theorem
theorem Th98:
begin
theorem Th99:
theorem
:: deftheorem defines being_quasi-order ORDERS_1:def 3 :
:: deftheorem Def4 defines being_partial-order ORDERS_1:def 4 :
:: deftheorem Def5 defines being_linear-order ORDERS_1:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
Lm3:
for R being Relation st R is connected holds
R ~ is connected
theorem Th106:
theorem
theorem
theorem Th109:
theorem
theorem
theorem
Lm4:
for R being Relation holds R c= [:(field R),(field R):]
Lm5:
for R being Relation
for X being set st R is reflexive & X c= field R holds
field (R |_2 X) = X
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th119:
theorem Th120:
:: deftheorem Def6 defines quasi_orders ORDERS_1:def 6 :
:: deftheorem Def7 defines partially_orders ORDERS_1:def 7 :
:: deftheorem defines linearly_orders ORDERS_1:def 8 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th124:
theorem Th125:
theorem
theorem Th127:
theorem
Lm6:
for R being Relation
for X being set st R is_reflexive_in X holds
R |_2 X is reflexive
Lm7:
for R being Relation
for X being set st R is_transitive_in X holds
R |_2 X is transitive
Lm8:
for R being Relation
for X being set st R is_antisymmetric_in X holds
R |_2 X is antisymmetric
Lm9:
for R being Relation
for X being set st R is_connected_in X holds
R |_2 X is connected
theorem
theorem Th130:
theorem
theorem
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
theorem
theorem
theorem
Lm11:
for R being Relation
for X being set st R is_reflexive_in X holds
R ~ is_reflexive_in X
Lm12:
for R being Relation
for X being set st R is_transitive_in X holds
R ~ is_transitive_in X
Lm13:
for R being Relation
for X being set st R is_antisymmetric_in X holds
R ~ is_antisymmetric_in X
Lm14:
for R being Relation
for X being set st R is_connected_in X holds
R ~ is_connected_in X
theorem
theorem Th137:
theorem
theorem
theorem
theorem Th141:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def9 defines has_upper_Zorn_property_wrt ORDERS_1:def 9 :
:: deftheorem defines has_lower_Zorn_property_wrt ORDERS_1:def 10 :
Lm15:
for R being Relation
for X being set holds (R |_2 X) ~ = (R ~ ) |_2 X
theorem
canceled;
theorem
canceled;
theorem Th149:
theorem
theorem Th151:
theorem
:: deftheorem Def11 defines is_maximal_in ORDERS_1:def 11 :
:: deftheorem Def12 defines is_minimal_in ORDERS_1:def 12 :
:: deftheorem Def13 defines is_superior_of ORDERS_1:def 13 :
:: deftheorem Def14 defines is_inferior_of ORDERS_1:def 14 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th163:
theorem
theorem
theorem
Lm17:
for R being Relation
for X, Y being set st R well_orders X & Y c= X holds
R well_orders Y
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th173:
theorem Th174:
theorem Th175:
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 ) )
theorem Th176:
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 ) )
theorem Th177:
theorem
scheme
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]
scheme
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]
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem Th196:
theorem