:: by Wojciech A. Trybulec

::

:: Received August 30, 1989

:: Copyright (c) 1990-2018 Association of Mizar Users

Lm1: for Y being set holds

( ex X being set st

( X <> {} & X in Y ) iff union Y <> {} )

proof end;

definition

let f be Function;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = the Element of f . x ) )

end;
mode Choice of f -> Function means :Def1: :: ORDERS_1:def 1

( dom it = dom f & ( for x being object st x in dom f holds

it . x = the Element of f . x ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = the Element of f . x ) );

ex b

( dom b

b

proof end;

:: deftheorem Def1 defines Choice ORDERS_1:def 1 :

for f, b_{2} being Function holds

( b_{2} is Choice of f iff ( dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = the Element of f . x ) ) );

for f, b

( b

b

definition

let I be set ;

let M be ManySortedSet of I;

for b_{1} being Choice of M holds b_{1} is ManySortedSet of I

for b_{1} being ManySortedSet of I holds

( b_{1} is Choice of M iff for x being object st x in I holds

b_{1} . x = the Element of M . x )

end;
let M be ManySortedSet of I;

:: original: Choice

redefine mode Choice of M -> ManySortedSet of I means :Def2: :: ORDERS_1:def 2

for x being object st x in I holds

it . x = the Element of M . x;

coherence redefine mode Choice of M -> ManySortedSet of I means :Def2: :: ORDERS_1:def 2

for x being object st x in I holds

it . x = the Element of M . x;

for b

proof end;

compatibility for b

( b

b

proof end;

:: deftheorem Def2 defines Choice ORDERS_1:def 2 :

for I being set

for M, b_{3} being ManySortedSet of I holds

( b_{3} is Choice of M iff for x being object st x in I holds

b_{3} . x = the Element of M . x );

for I being set

for M, b

( b

b

Lm2: for M being non empty set st not {} in M holds

for Ch being Choice_Function of M

for X being set st X in M holds

Ch . X in X

proof end;

Lm3: for M being non empty set st not {} in M holds

for Ch being Choice_Function of M holds Ch is Function of M,(union M)

proof end;

registration
end;

::

:: Orders.

::

:: Orders.

::

definition
end;

Lm4: for X being set

for R being total Relation of X holds field R = X

proof end;

theorem :: ORDERS_1:4

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

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

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

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

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 & P is_connected_in X ) )

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 :: ORDERS_1:8

theorem :: ORDERS_1:9

for X, Y being set

for P being Relation st P is_antisymmetric_in X & Y c= X holds

P is_antisymmetric_in Y ;

for P being Relation st P is_antisymmetric_in X & Y c= X holds

P is_antisymmetric_in Y ;

theorem :: ORDERS_1:10

for X, Y being set

for P being Relation st P is_transitive_in X & Y c= X holds

P is_transitive_in Y ;

for P being Relation st P is_transitive_in X & Y c= X holds

P is_transitive_in Y ;

theorem :: ORDERS_1:11

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 ;

for P being Relation st P is_strongly_connected_in X & Y c= X holds

P is_strongly_connected_in Y ;

::

:: Orders.

::

:: Orders.

::

definition

let R be Relation;

end;
attr R is being_partial-order means :: ORDERS_1:def 5

( R is reflexive & R is transitive & R is antisymmetric );

( R is reflexive & R is transitive & R is antisymmetric );

attr R is being_linear-order means :: ORDERS_1:def 6

( R is reflexive & R is transitive & R is antisymmetric & R is connected );

( R is reflexive & R is transitive & R is antisymmetric & R is connected );

:: deftheorem defines being_quasi-order ORDERS_1:def 4 :

for R being Relation holds

( R is being_quasi-order iff ( R is reflexive & R is transitive ) );

for R being Relation holds

( R is being_quasi-order iff ( R is reflexive & R is transitive ) );

:: deftheorem defines being_partial-order ORDERS_1:def 5 :

for R being Relation holds

( R is being_partial-order iff ( R is reflexive & R is transitive & R is antisymmetric ) );

for R being Relation holds

( R is being_partial-order iff ( R is reflexive & R is transitive & R is antisymmetric ) );

:: deftheorem defines being_linear-order ORDERS_1:def 6 :

for R being Relation holds

( R is being_linear-order iff ( R is reflexive & R is transitive & R is antisymmetric & R is connected ) );

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

theorem :: ORDERS_1:17

Lm5: for R being Relation st R is connected holds

R ~ is connected

proof end;

theorem :: ORDERS_1:19

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

( R is being_quasi-order & R is being_partial-order & R is being_linear-order ) ;

theorem :: ORDERS_1:20

for R being Relation st R is being_linear-order holds

( R is being_quasi-order & R is being_partial-order ) ;

( R is being_quasi-order & R is being_partial-order ) ;

theorem :: ORDERS_1:21

theorem :: ORDERS_1:24

Lm6: for R being Relation holds R c= [:(field R),(field R):]

proof end;

Lm7: 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:25

for R being Relation

for X being set st R is being_quasi-order holds

R |_2 X is being_quasi-order by WELLORD1:15, WELLORD1:17;

for X being set st R is being_quasi-order holds

R |_2 X is being_quasi-order by WELLORD1:15, WELLORD1:17;

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 by WELLORD1:15, WELLORD1:17;

for X being set st R is being_partial-order holds

R |_2 X is being_partial-order by WELLORD1:15, WELLORD1:17;

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 by WELLORD1:15, WELLORD1:16, WELLORD1:17;

for X being set st R is being_linear-order holds

R |_2 X is being_linear-order by WELLORD1:15, WELLORD1:16, WELLORD1:17;

registration

for b_{1} being Relation st b_{1} is empty holds

( b_{1} is being_quasi-order & b_{1} is being_partial-order & b_{1} is being_linear-order & b_{1} is well-ordering )
end;

cluster empty Relation-like -> well-ordering being_quasi-order being_partial-order being_linear-order for Relation;

coherence for b

( b

proof end;

registration
end;

definition

let R be Relation;

let X be set ;

end;
let X be set ;

pred R partially_orders X means :: ORDERS_1:def 8

( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X );

( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X );

pred R linearly_orders X means :: ORDERS_1:def 9

( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X );

( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X );

:: deftheorem defines quasi_orders ORDERS_1:def 7 :

for R being Relation

for X being set holds

( R quasi_orders X iff ( R is_reflexive_in X & R is_transitive_in X ) );

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 defines partially_orders ORDERS_1:def 8 :

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

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

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

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 Th28: :: ORDERS_1:28

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

for X being set st R well_orders X holds

( R quasi_orders X & R partially_orders X & R linearly_orders X ) ;

theorem Th29: :: ORDERS_1:29

for R being Relation

for X being set st R linearly_orders X holds

( R quasi_orders X & R partially_orders X ) ;

for X being set st R linearly_orders X holds

( R quasi_orders X & R partially_orders X ) ;

theorem :: ORDERS_1:30

Lm8: for R being Relation

for X being set st R is_reflexive_in X holds

R |_2 X is reflexive

proof end;

Lm9: for R being Relation

for X being set st R is_transitive_in X holds

R |_2 X is transitive

proof end;

Lm10: for R being Relation

for X being set st R is_antisymmetric_in X holds

R |_2 X is antisymmetric

proof end;

Lm11: 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:33

for R being Relation

for X being set st R quasi_orders X holds

R |_2 X is being_quasi-order by Lm8, Lm9;

for X being set st R quasi_orders X holds

R |_2 X is being_quasi-order by Lm8, Lm9;

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 by Lm8, Lm9, Lm10;

for X being set st R partially_orders X holds

R |_2 X is being_partial-order by Lm8, Lm9, Lm10;

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 by Lm8, Lm9, Lm10, Lm11;

for X being set st R linearly_orders X holds

R |_2 X is being_linear-order by Lm8, Lm9, Lm10, Lm11;

Lm12: for R being Relation

for X being set st R is_reflexive_in X holds

R ~ is_reflexive_in X

proof end;

Lm13: for R being Relation

for X being set st R is_transitive_in X holds

R ~ is_transitive_in X

proof end;

Lm14: for R being Relation

for X being set st R is_antisymmetric_in X holds

R ~ is_antisymmetric_in X

proof end;

Lm15: 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:40

theorem Th41: :: ORDERS_1:41

for R being Relation

for X being set st R partially_orders X holds

R ~ partially_orders X by Lm12, Lm13, Lm14;

for X being set st R partially_orders X holds

R ~ partially_orders X by Lm12, Lm13, Lm14;

theorem :: ORDERS_1:42

for R being Relation

for X being set st R linearly_orders X holds

R ~ linearly_orders X by Lm12, Lm13, Lm14, Lm15;

for X being set st R linearly_orders X holds

R ~ linearly_orders X by Lm12, Lm13, Lm14, Lm15;

theorem :: ORDERS_1:46

theorem :: ORDERS_1:47

definition

let R be Relation;

let X be set ;

end;
let X be set ;

pred X has_upper_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

[y,x] in R ) );

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 11

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

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

:: deftheorem defines has_upper_Zorn_property_wrt ORDERS_1:def 10 :

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

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

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

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

Lm16: for R being Relation

for X being set holds (R |_2 X) ~ = (R ~) |_2 X

proof end;

Lm17: 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;
thus R |_2 {} = ({} |` R) | {} by WELLORD1:10

.= {} ; :: thesis: verum

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

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

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 ;

end;
let x be set ;

pred x is_maximal_in R means :: ORDERS_1:def 12

( x in field R & ( for y being set holds

( not y in field R or not y <> x or not [x,y] in R ) ) );

( 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 :: ORDERS_1:def 13

( x in field R & ( for y being set holds

( not y in field R or not y <> x or not [y,x] in R ) ) );

( 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 defines is_maximal_in ORDERS_1:def 12 :

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

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 defines is_minimal_in ORDERS_1:def 13 :

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

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 defines is_superior_of ORDERS_1:def 14 :

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

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 defines is_inferior_of ORDERS_1:def 15 :

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

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

for R being Relation

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

x is_minimal_in R

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

x is_minimal_in R

proof end;

theorem :: ORDERS_1:54

for R being Relation

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

x is_maximal_in R

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

x is_maximal_in R

proof end;

theorem :: ORDERS_1:57

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

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

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

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;

Lm18: 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 Th63: :: ORDERS_1:63

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

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 Th64: :: ORDERS_1:64

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

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 Th65: :: ORDERS_1:65

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

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 Th66: :: ORDERS_1:66

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

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 Th67: :: ORDERS_1:67

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

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

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

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_{1}() -> non empty set , P_{1}[ set , set ] } :

provided

ZornMax{ F

provided

A1:
for x being Element of F_{1}() holds P_{1}[x,x]
and

A2: for x, y being Element of F_{1}() st P_{1}[x,y] & P_{1}[y,x] holds

x = y and

A3: for x, y, z being Element of F_{1}() st P_{1}[x,y] & P_{1}[y,z] holds

P_{1}[x,z]
and

A4: for X being set st X c= F_{1}() & ( for x, y being Element of F_{1}() st x in X & y in X & P_{1}[x,y] holds

P_{1}[y,x] ) holds

ex y being Element of F_{1}() st

for x being Element of F_{1}() st x in X holds

P_{1}[x,y]

A2: for x, y being Element of F

x = y and

A3: for x, y, z being Element of F

P

A4: for X being set st X c= F

P

ex y being Element of F

for x being Element of F

P

proof end;

scheme :: ORDERS_1:sch 2

ZornMin{ F_{1}() -> non empty set , P_{1}[ set , set ] } :

provided

ZornMin{ F

provided

A1:
for x being Element of F_{1}() holds P_{1}[x,x]
and

A2: for x, y being Element of F_{1}() st P_{1}[x,y] & P_{1}[y,x] holds

x = y and

A3: for x, y, z being Element of F_{1}() st P_{1}[x,y] & P_{1}[y,z] holds

P_{1}[x,z]
and

A4: for X being set st X c= F_{1}() & ( for x, y being Element of F_{1}() st x in X & y in X & P_{1}[x,y] holds

P_{1}[y,x] ) holds

ex y being Element of F_{1}() st

for x being Element of F_{1}() st x in X holds

P_{1}[y,x]

A2: for x, y being Element of F

x = y and

A3: for x, y, z being Element of F

P

A4: for X being set st X c= F

P

ex y being Element of F

for x being Element of F

P

proof end;

::

:: Orders - continuation.

::

:: Orders - continuation.

::

theorem :: ORDERS_1:69

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 )

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;

::

:: Auxiliary theorems.

::

:: Auxiliary theorems.

::

theorem :: ORDERS_1:71

theorem :: ORDERS_1:72

theorem :: ORDERS_1:73

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

for X being set st R is_antisymmetric_in X holds

R |_2 X is antisymmetric by Lm10;

theorem :: ORDERS_1:75

theorem :: ORDERS_1:76

theorem :: ORDERS_1:77

theorem :: ORDERS_1:79

theorem :: ORDERS_1:80

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

for X being set st R is_antisymmetric_in X holds

R ~ is_antisymmetric_in X by Lm14;

theorem :: ORDERS_1:82

theorem :: ORDERS_1:83

:: from COMPTS_1

theorem :: ORDERS_1:85

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 )

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;

:: from AMISTD_3, 2006.03.26, A.T.

:: from AMISTD_3, 2010.01.10, A.T

registration
end;

definition

let X be set ;

:: original: RelIncl

redefine func RelIncl X -> Order of X;

coherence

RelIncl X is Order of X

end;
:: original: RelIncl

redefine func RelIncl X -> Order of X;

coherence

RelIncl X is Order of X

proof end;

theorem :: ORDERS_1:89

theorem :: ORDERS_1:90

:: Choice function.

::