begin
Lm1:
for Y being set holds
( ex X being set st
( X <> {} & X in Y ) iff union Y <> {} )
Lm2:
for X being set
for R being total Relation of X holds field R = X
begin
Lm3:
for R being Relation st R is connected holds
R ~ is connected
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
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
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
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
Lm15:
for R being Relation
for X being set holds (R |_2 X) ~ = (R ~) |_2 X
Lm17:
for R being Relation
for X, Y being set st R well_orders X & Y c= X holds
R well_orders Y
theorem Th65:
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 Th66:
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 ) )
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]
begin
:: Orders.
::