:: by Grzegorz Bancerek

::

:: Received September 10, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

definition

let A be non empty RelStr ;

compatibility

( A is reflexive iff for x being Element of A holds x <= x )

end;
compatibility

( A is reflexive iff for x being Element of A holds x <= x )

proof end;

:: deftheorem defines reflexive YELLOW_0:def 1 :

for A being non empty RelStr holds

( A is reflexive iff for x being Element of A holds x <= x );

for A being non empty RelStr holds

( A is reflexive iff for x being Element of A holds x <= x );

definition

let A be RelStr ;

( A is transitive iff for x, y, z being Element of A st x <= y & y <= z holds

x <= z )

( A is antisymmetric iff for x, y being Element of A st x <= y & y <= x holds

x = y )

end;
redefine attr A is transitive means :: YELLOW_0:def 2

for x, y, z being Element of A st x <= y & y <= z holds

x <= z;

compatibility for x, y, z being Element of A st x <= y & y <= z holds

x <= z;

( A is transitive iff for x, y, z being Element of A st x <= y & y <= z holds

x <= z )

proof end;

redefine attr A is antisymmetric means :: YELLOW_0:def 3

for x, y being Element of A st x <= y & y <= x holds

x = y;

compatibility for x, y being Element of A st x <= y & y <= x holds

x = y;

( A is antisymmetric iff for x, y being Element of A st x <= y & y <= x holds

x = y )

proof end;

:: deftheorem defines transitive YELLOW_0:def 2 :

for A being RelStr holds

( A is transitive iff for x, y, z being Element of A st x <= y & y <= z holds

x <= z );

for A being RelStr holds

( A is transitive iff for x, y, z being Element of A st x <= y & y <= z holds

x <= z );

:: deftheorem defines antisymmetric YELLOW_0:def 3 :

for A being RelStr holds

( A is antisymmetric iff for x, y being Element of A st x <= y & y <= x holds

x = y );

for A being RelStr holds

( A is antisymmetric iff for x, y being Element of A st x <= y & y <= x holds

x = y );

registration

coherence

for b_{1} being non empty RelStr st b_{1} is complete holds

( b_{1} is with_suprema & b_{1} is with_infima )
by LATTICE3:12;

coherence

for b_{1} being 1 -element reflexive RelStr holds

( b_{1} is complete & b_{1} is transitive & b_{1} is antisymmetric )

end;
for b

( b

coherence

for b

( b

proof end;

registration
end;

registration

existence

ex b_{1} being RelStr st

( b_{1} is strict & b_{1} is 1 -element & b_{1} is reflexive )

end;
ex b

( b

proof end;

theorem Th1: :: YELLOW_0:1

for P1, P2 being RelStr st RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) holds

for a1, b1 being Element of P1

for a2, b2 being Element of P2 st a1 = a2 & b1 = b2 holds

( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) )

for a1, b1 being Element of P1

for a2, b2 being Element of P2 st a1 = a2 & b1 = b2 holds

( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) )

proof end;

theorem Th2: :: YELLOW_0:2

for P1, P2 being RelStr st RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) holds

for X being set

for a1 being Element of P1

for a2 being Element of P2 st a1 = a2 holds

( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) )

for X being set

for a1 being Element of P1

for a2 being Element of P2 st a1 = a2 holds

( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) )

proof end;

theorem :: YELLOW_0:3

for P1, P2 being RelStr st RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) & P1 is complete holds

P2 is complete

P2 is complete

proof end;

theorem Th4: :: YELLOW_0:4

for L being transitive RelStr

for x, y being Element of L st x <= y holds

for X being set holds

( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) )

for x, y being Element of L st x <= y holds

for X being set holds

( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) )

proof end;

theorem Th5: :: YELLOW_0:5

for L being non empty RelStr

for X being set

for x being Element of L holds

( ( x is_>=_than X implies x is_>=_than X /\ the carrier of L ) & ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) )

for X being set

for x being Element of L holds

( ( x is_>=_than X implies x is_>=_than X /\ the carrier of L ) & ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) )

proof end;

theorem Th7: :: YELLOW_0:7

for L being RelStr

for a, b being Element of L holds

( ( a is_<=_than {b} implies a <= b ) & ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) )

for a, b being Element of L holds

( ( a is_<=_than {b} implies a <= b ) & ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) )

proof end;

theorem Th8: :: YELLOW_0:8

for L being RelStr

for a, b, c being Element of L holds

( ( a is_<=_than {b,c} implies ( a <= b & a <= c ) ) & ( a <= b & a <= c implies a is_<=_than {b,c} ) & ( a is_>=_than {b,c} implies ( b <= a & c <= a ) ) & ( b <= a & c <= a implies a is_>=_than {b,c} ) )

for a, b, c being Element of L holds

( ( a is_<=_than {b,c} implies ( a <= b & a <= c ) ) & ( a <= b & a <= c implies a is_<=_than {b,c} ) & ( a is_>=_than {b,c} implies ( b <= a & c <= a ) ) & ( b <= a & c <= a implies a is_>=_than {b,c} ) )

proof end;

theorem Th9: :: YELLOW_0:9

for L being RelStr

for X, Y being set st X c= Y holds

for x being Element of L holds

( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) )

for X, Y being set st X c= Y holds

for x being Element of L holds

( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) )

proof end;

theorem Th10: :: YELLOW_0:10

for L being RelStr

for X, Y being set

for x being Element of L holds

( ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) & ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y ) )

for X, Y being set

for x being Element of L holds

( ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) & ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y ) )

proof end;

theorem Th11: :: YELLOW_0:11

for L being transitive RelStr

for X being set

for x, y being Element of L st X is_<=_than x & x <= y holds

X is_<=_than y

for X being set

for x, y being Element of L st X is_<=_than x & x <= y holds

X is_<=_than y

proof end;

theorem Th12: :: YELLOW_0:12

for L being transitive RelStr

for X being set

for x, y being Element of L st X is_>=_than x & x >= y holds

X is_>=_than y

for X being set

for x, y being Element of L st X is_>=_than x & x >= y holds

X is_>=_than y

proof end;

registration
end;

begin

definition

let L be RelStr ;

end;
attr L is lower-bounded means :Def4: :: YELLOW_0:def 4

ex x being Element of L st x is_<=_than the carrier of L;

ex x being Element of L st x is_<=_than the carrier of L;

attr L is upper-bounded means :Def5: :: YELLOW_0:def 5

ex x being Element of L st x is_>=_than the carrier of L;

ex x being Element of L st x is_>=_than the carrier of L;

:: deftheorem Def4 defines lower-bounded YELLOW_0:def 4 :

for L being RelStr holds

( L is lower-bounded iff ex x being Element of L st x is_<=_than the carrier of L );

for L being RelStr holds

( L is lower-bounded iff ex x being Element of L st x is_<=_than the carrier of L );

:: deftheorem Def5 defines upper-bounded YELLOW_0:def 5 :

for L being RelStr holds

( L is upper-bounded iff ex x being Element of L st x is_>=_than the carrier of L );

for L being RelStr holds

( L is upper-bounded iff ex x being Element of L st x is_>=_than the carrier of L );

:: deftheorem defines bounded YELLOW_0:def 6 :

for L being RelStr holds

( L is bounded iff ( L is lower-bounded & L is upper-bounded ) );

for L being RelStr holds

( L is bounded iff ( L is lower-bounded & L is upper-bounded ) );

theorem :: YELLOW_0:13

for P1, P2 being RelStr st RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) holds

( ( P1 is lower-bounded implies P2 is lower-bounded ) & ( P1 is upper-bounded implies P2 is upper-bounded ) )

( ( P1 is lower-bounded implies P2 is lower-bounded ) & ( P1 is upper-bounded implies P2 is upper-bounded ) )

proof end;

registration

coherence

for b_{1} being non empty RelStr st b_{1} is complete holds

b_{1} is bounded

for b_{1} being RelStr st b_{1} is bounded holds

( b_{1} is lower-bounded & b_{1} is upper-bounded )

for b_{1} being RelStr st b_{1} is lower-bounded & b_{1} is upper-bounded holds

b_{1} is bounded

end;
for b

b

proof end;

coherence for b

( b

proof end;

coherence for b

b

proof end;

definition

let L be RelStr ;

let X be set ;

end;
let X be set ;

pred ex_sup_of X,L means :Def7: :: YELLOW_0:def 7

ex a being Element of L st

( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds

b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds

b >= c ) holds

c = a ) );

ex a being Element of L st

( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds

b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds

b >= c ) holds

c = a ) );

pred ex_inf_of X,L means :Def8: :: YELLOW_0:def 8

ex a being Element of L st

( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds

b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds

b <= c ) holds

c = a ) );

ex a being Element of L st

( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds

b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds

b <= c ) holds

c = a ) );

:: deftheorem Def7 defines ex_sup_of YELLOW_0:def 7 :

for L being RelStr

for X being set holds

( ex_sup_of X,L iff ex a being Element of L st

( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds

b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds

b >= c ) holds

c = a ) ) );

for L being RelStr

for X being set holds

( ex_sup_of X,L iff ex a being Element of L st

( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds

b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds

b >= c ) holds

c = a ) ) );

:: deftheorem Def8 defines ex_inf_of YELLOW_0:def 8 :

for L being RelStr

for X being set holds

( ex_inf_of X,L iff ex a being Element of L st

( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds

b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds

b <= c ) holds

c = a ) ) );

for L being RelStr

for X being set holds

( ex_inf_of X,L iff ex a being Element of L st

( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds

b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds

b <= c ) holds

c = a ) ) );

theorem Th14: :: YELLOW_0:14

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds

for X being set holds

( ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) & ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) )

for X being set holds

( ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) & ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) )

proof end;

theorem Th15: :: YELLOW_0:15

for L being antisymmetric RelStr

for X being set holds

( ex_sup_of X,L iff ex a being Element of L st

( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds

a <= b ) ) )

for X being set holds

( ex_sup_of X,L iff ex a being Element of L st

( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds

a <= b ) ) )

proof end;

theorem Th16: :: YELLOW_0:16

for L being antisymmetric RelStr

for X being set holds

( ex_inf_of X,L iff ex a being Element of L st

( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds

a >= b ) ) )

for X being set holds

( ex_inf_of X,L iff ex a being Element of L st

( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds

a >= b ) ) )

proof end;

theorem Th17: :: YELLOW_0:17

for L being non empty antisymmetric complete RelStr

for X being set holds

( ex_sup_of X,L & ex_inf_of X,L )

for X being set holds

( ex_sup_of X,L & ex_inf_of X,L )

proof end;

theorem Th18: :: YELLOW_0:18

for L being antisymmetric RelStr

for a, b, c being Element of L holds

( c = a "\/" b & ex_sup_of {a,b},L iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds

c <= d ) ) )

for a, b, c being Element of L holds

( c = a "\/" b & ex_sup_of {a,b},L iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds

c <= d ) ) )

proof end;

theorem Th19: :: YELLOW_0:19

for L being antisymmetric RelStr

for a, b, c being Element of L holds

( c = a "/\" b & ex_inf_of {a,b},L iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds

c >= d ) ) )

for a, b, c being Element of L holds

( c = a "/\" b & ex_inf_of {a,b},L iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds

c >= d ) ) )

proof end;

theorem Th20: :: YELLOW_0:20

for L being antisymmetric RelStr holds

( L is with_suprema iff for a, b being Element of L holds ex_sup_of {a,b},L )

( L is with_suprema iff for a, b being Element of L holds ex_sup_of {a,b},L )

proof end;

theorem Th21: :: YELLOW_0:21

for L being antisymmetric RelStr holds

( L is with_infima iff for a, b being Element of L holds ex_inf_of {a,b},L )

( L is with_infima iff for a, b being Element of L holds ex_inf_of {a,b},L )

proof end;

theorem Th22: :: YELLOW_0:22

for L being antisymmetric with_suprema RelStr

for a, b, c being Element of L holds

( c = a "\/" b iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds

c <= d ) ) )

for a, b, c being Element of L holds

( c = a "\/" b iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds

c <= d ) ) )

proof end;

theorem Th23: :: YELLOW_0:23

for L being antisymmetric with_infima RelStr

for a, b, c being Element of L holds

( c = a "/\" b iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds

c >= d ) ) )

for a, b, c being Element of L holds

( c = a "/\" b iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds

c >= d ) ) )

proof end;

theorem :: YELLOW_0:24

for L being reflexive antisymmetric with_suprema RelStr

for a, b being Element of L holds

( a = a "\/" b iff a >= b )

for a, b being Element of L holds

( a = a "\/" b iff a >= b )

proof end;

theorem :: YELLOW_0:25

for L being reflexive antisymmetric with_infima RelStr

for a, b being Element of L holds

( a = a "/\" b iff a <= b )

for a, b being Element of L holds

( a = a "/\" b iff a <= b )

proof end;

definition

let L be RelStr ;

let X be set ;

for b_{1}, b_{2} being Element of L st ex_sup_of X,L & X is_<=_than b_{1} & ( for a being Element of L st X is_<=_than a holds

b_{1} <= a ) & X is_<=_than b_{2} & ( for a being Element of L st X is_<=_than a holds

b_{2} <= a ) holds

b_{1} = b_{2}

( ex_sup_of X,L implies ex b_{1} being Element of L st

( X is_<=_than b_{1} & ( for a being Element of L st X is_<=_than a holds

b_{1} <= a ) ) )

consistency

for b_{1} being Element of L holds verum;

;

for b_{1}, b_{2} being Element of L st ex_inf_of X,L & X is_>=_than b_{1} & ( for a being Element of L st X is_>=_than a holds

a <= b_{1} ) & X is_>=_than b_{2} & ( for a being Element of L st X is_>=_than a holds

a <= b_{2} ) holds

b_{1} = b_{2}

( ex_inf_of X,L implies ex b_{1} being Element of L st

( X is_>=_than b_{1} & ( for a being Element of L st X is_>=_than a holds

a <= b_{1} ) ) )

consistency

for b_{1} being Element of L holds verum;

;

end;
let X be set ;

func "\/" (X,L) -> Element of L means :Def9: :: YELLOW_0:def 9

( X is_<=_than it & ( for a being Element of L st X is_<=_than a holds

it <= a ) ) if ex_sup_of X,L

;

uniqueness ( X is_<=_than it & ( for a being Element of L st X is_<=_than a holds

it <= a ) ) if ex_sup_of X,L

;

for b

b

b

b

proof end;

existence ( ex_sup_of X,L implies ex b

( X is_<=_than b

b

proof end;

correctness consistency

for b

;

func "/\" (X,L) -> Element of L means :Def10: :: YELLOW_0:def 10

( X is_>=_than it & ( for a being Element of L st X is_>=_than a holds

a <= it ) ) if ex_inf_of X,L

;

uniqueness ( X is_>=_than it & ( for a being Element of L st X is_>=_than a holds

a <= it ) ) if ex_inf_of X,L

;

for b

a <= b

a <= b

b

proof end;

existence ( ex_inf_of X,L implies ex b

( X is_>=_than b

a <= b

proof end;

correctness consistency

for b

;

:: deftheorem Def9 defines "\/" YELLOW_0:def 9 :

for L being RelStr

for X being set

for b_{3} being Element of L st ex_sup_of X,L holds

( b_{3} = "\/" (X,L) iff ( X is_<=_than b_{3} & ( for a being Element of L st X is_<=_than a holds

b_{3} <= a ) ) );

for L being RelStr

for X being set

for b

( b

b

:: deftheorem Def10 defines "/\" YELLOW_0:def 10 :

for L being RelStr

for X being set

for b_{3} being Element of L st ex_inf_of X,L holds

( b_{3} = "/\" (X,L) iff ( X is_>=_than b_{3} & ( for a being Element of L st X is_>=_than a holds

a <= b_{3} ) ) );

for L being RelStr

for X being set

for b

( b

a <= b

theorem :: YELLOW_0:26

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds

for X being set st ex_sup_of X,L1 holds

"\/" (X,L1) = "\/" (X,L2)

for X being set st ex_sup_of X,L1 holds

"\/" (X,L1) = "\/" (X,L2)

proof end;

theorem :: YELLOW_0:27

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds

for X being set st ex_inf_of X,L1 holds

"/\" (X,L1) = "/\" (X,L2)

for X being set st ex_inf_of X,L1 holds

"/\" (X,L1) = "/\" (X,L2)

proof end;

theorem :: YELLOW_0:28

for L being non empty complete Poset

for X being set holds

( "\/" (X,L) = "\/" (X,(latt L)) & "/\" (X,L) = "/\" (X,(latt L)) )

for X being set holds

( "\/" (X,L) = "\/" (X,(latt L)) & "/\" (X,L) = "/\" (X,(latt L)) )

proof end;

theorem :: YELLOW_0:29

for L being complete Lattice

for X being set holds

( "\/" (X,L) = "\/" (X,(LattPOSet L)) & "/\" (X,L) = "/\" (X,(LattPOSet L)) )

for X being set holds

( "\/" (X,L) = "\/" (X,(LattPOSet L)) & "/\" (X,L) = "/\" (X,(LattPOSet L)) )

proof end;

theorem Th30: :: YELLOW_0:30

for L being antisymmetric RelStr

for a being Element of L

for X being set holds

( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds

a <= b ) ) )

for a being Element of L

for X being set holds

( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds

a <= b ) ) )

proof end;

theorem Th31: :: YELLOW_0:31

for L being antisymmetric RelStr

for a being Element of L

for X being set holds

( a = "/\" (X,L) & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds

a >= b ) ) )

for a being Element of L

for X being set holds

( a = "/\" (X,L) & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds

a >= b ) ) )

proof end;

theorem :: YELLOW_0:32

for L being non empty antisymmetric complete RelStr

for a being Element of L

for X being set holds

( a = "\/" (X,L) iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds

a <= b ) ) )

for a being Element of L

for X being set holds

( a = "\/" (X,L) iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds

a <= b ) ) )

proof end;

theorem :: YELLOW_0:33

for L being non empty antisymmetric complete RelStr

for a being Element of L

for X being set holds

( a = "/\" (X,L) iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds

a >= b ) ) )

for a being Element of L

for X being set holds

( a = "/\" (X,L) iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds

a >= b ) ) )

proof end;

theorem Th34: :: YELLOW_0:34

for L being RelStr

for X, Y being set st X c= Y & ex_sup_of X,L & ex_sup_of Y,L holds

"\/" (X,L) <= "\/" (Y,L)

for X, Y being set st X c= Y & ex_sup_of X,L & ex_sup_of Y,L holds

"\/" (X,L) <= "\/" (Y,L)

proof end;

theorem Th35: :: YELLOW_0:35

for L being RelStr

for X, Y being set st X c= Y & ex_inf_of X,L & ex_inf_of Y,L holds

"/\" (X,L) >= "/\" (Y,L)

for X, Y being set st X c= Y & ex_inf_of X,L & ex_inf_of Y,L holds

"/\" (X,L) >= "/\" (Y,L)

proof end;

theorem :: YELLOW_0:36

for L being transitive antisymmetric RelStr

for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L & ex_sup_of X \/ Y,L holds

"\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L))

for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L & ex_sup_of X \/ Y,L holds

"\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L))

proof end;

theorem :: YELLOW_0:37

for L being transitive antisymmetric RelStr

for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L & ex_inf_of X \/ Y,L holds

"/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L))

for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L & ex_inf_of X \/ Y,L holds

"/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L))

proof end;

notation
end;

theorem Th38: :: YELLOW_0:38

for L being non empty reflexive antisymmetric RelStr

for a being Element of L holds

( ex_sup_of {a},L & ex_inf_of {a},L )

for a being Element of L holds

( ex_sup_of {a},L & ex_inf_of {a},L )

proof end;

theorem :: YELLOW_0:39

for L being non empty reflexive antisymmetric RelStr

for a being Element of L holds

( sup {a} = a & inf {a} = a )

for a being Element of L holds

( sup {a} = a & inf {a} = a )

proof end;

theorem Th42: :: YELLOW_0:42

for L being non empty antisymmetric lower-bounded RelStr holds

( ex_sup_of {} ,L & ex_inf_of the carrier of L,L )

( ex_sup_of {} ,L & ex_inf_of the carrier of L,L )

proof end;

theorem Th43: :: YELLOW_0:43

for L being non empty antisymmetric upper-bounded RelStr holds

( ex_inf_of {} ,L & ex_sup_of the carrier of L,L )

( ex_inf_of {} ,L & ex_sup_of the carrier of L,L )

proof end;

definition

let L be RelStr ;

correctness

coherence

"\/" ({},L) is Element of L;

;

correctness

coherence

"/\" ({},L) is Element of L;

;

end;
correctness

coherence

"\/" ({},L) is Element of L;

;

correctness

coherence

"/\" ({},L) is Element of L;

;

theorem :: YELLOW_0:44

for L being non empty antisymmetric lower-bounded RelStr

for x being Element of L holds Bottom L <= x

for x being Element of L holds Bottom L <= x

proof end;

theorem Th46: :: YELLOW_0:46

for L being non empty RelStr

for X, Y being set st ( for x being Element of L holds

( x is_>=_than X iff x is_>=_than Y ) ) & ex_sup_of X,L holds

ex_sup_of Y,L

for X, Y being set st ( for x being Element of L holds

( x is_>=_than X iff x is_>=_than Y ) ) & ex_sup_of X,L holds

ex_sup_of Y,L

proof end;

theorem Th47: :: YELLOW_0:47

for L being non empty RelStr

for X, Y being set st ex_sup_of X,L & ( for x being Element of L holds

( x is_>=_than X iff x is_>=_than Y ) ) holds

"\/" (X,L) = "\/" (Y,L)

for X, Y being set st ex_sup_of X,L & ( for x being Element of L holds

( x is_>=_than X iff x is_>=_than Y ) ) holds

"\/" (X,L) = "\/" (Y,L)

proof end;

theorem Th48: :: YELLOW_0:48

for L being non empty RelStr

for X, Y being set st ( for x being Element of L holds

( x is_<=_than X iff x is_<=_than Y ) ) & ex_inf_of X,L holds

ex_inf_of Y,L

for X, Y being set st ( for x being Element of L holds

( x is_<=_than X iff x is_<=_than Y ) ) & ex_inf_of X,L holds

ex_inf_of Y,L

proof end;

theorem Th49: :: YELLOW_0:49

for L being non empty RelStr

for X, Y being set st ex_inf_of X,L & ( for x being Element of L holds

( x is_<=_than X iff x is_<=_than Y ) ) holds

"/\" (X,L) = "/\" (Y,L)

for X, Y being set st ex_inf_of X,L & ( for x being Element of L holds

( x is_<=_than X iff x is_<=_than Y ) ) holds

"/\" (X,L) = "/\" (Y,L)

proof end;

theorem Th50: :: YELLOW_0:50

for L being non empty RelStr

for X being set holds

( ( ex_sup_of X,L implies ex_sup_of X /\ the carrier of L,L ) & ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) & ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) & ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) )

for X being set holds

( ( ex_sup_of X,L implies ex_sup_of X /\ the carrier of L,L ) & ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) & ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) & ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) )

proof end;

theorem :: YELLOW_0:51

for L being non empty RelStr

for X being set st ( ex_sup_of X,L or ex_sup_of X /\ the carrier of L,L ) holds

"\/" (X,L) = "\/" ((X /\ the carrier of L),L)

for X being set st ( ex_sup_of X,L or ex_sup_of X /\ the carrier of L,L ) holds

"\/" (X,L) = "\/" ((X /\ the carrier of L),L)

proof end;

theorem :: YELLOW_0:52

for L being non empty RelStr

for X being set st ( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L ) holds

"/\" (X,L) = "/\" ((X /\ the carrier of L),L)

for X being set st ( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L ) holds

"/\" (X,L) = "/\" ((X /\ the carrier of L),L)

proof end;

theorem :: YELLOW_0:54

for L being non empty Poset holds

( L is with_suprema iff for X being non empty finite Subset of L holds ex_sup_of X,L )

( L is with_suprema iff for X being non empty finite Subset of L holds ex_sup_of X,L )

proof end;

theorem :: YELLOW_0:55

for L being non empty Poset holds

( L is with_infima iff for X being non empty finite Subset of L holds ex_inf_of X,L )

( L is with_infima iff for X being non empty finite Subset of L holds ex_inf_of X,L )

proof end;

begin

definition

let L be RelStr ;

ex b_{1} being RelStr st

( the carrier of b_{1} c= the carrier of L & the InternalRel of b_{1} c= the InternalRel of L )
;

end;
mode SubRelStr of L -> RelStr means :Def13: :: YELLOW_0:def 13

( the carrier of it c= the carrier of L & the InternalRel of it c= the InternalRel of L );

existence ( the carrier of it c= the carrier of L & the InternalRel of it c= the InternalRel of L );

ex b

( the carrier of b

:: deftheorem Def13 defines SubRelStr YELLOW_0:def 13 :

for L, b_{2} being RelStr holds

( b_{2} is SubRelStr of L iff ( the carrier of b_{2} c= the carrier of L & the InternalRel of b_{2} c= the InternalRel of L ) );

for L, b

( b

definition

let L be RelStr ;

let S be SubRelStr of L;

end;
let S be SubRelStr of L;

attr S is full means :Def14: :: YELLOW_0:def 14

the InternalRel of S = the InternalRel of L |_2 the carrier of S;

the InternalRel of S = the InternalRel of L |_2 the carrier of S;

:: deftheorem Def14 defines full YELLOW_0:def 14 :

for L being RelStr

for S being SubRelStr of L holds

( S is full iff the InternalRel of S = the InternalRel of L |_2 the carrier of S );

for L being RelStr

for S being SubRelStr of L holds

( S is full iff the InternalRel of S = the InternalRel of L |_2 the carrier of S );

registration

let L be RelStr ;

existence

ex b_{1} being SubRelStr of L st

( b_{1} is strict & b_{1} is full )

end;
existence

ex b

( b

proof end;

registration

let L be non empty RelStr ;

existence

ex b_{1} being SubRelStr of L st

( not b_{1} is empty & b_{1} is full & b_{1} is strict )

end;
existence

ex b

( not b

proof end;

theorem Th56: :: YELLOW_0:56

for L being RelStr

for X being Subset of L holds RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L

for X being Subset of L holds RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L

proof end;

theorem Th57: :: YELLOW_0:57

for L being RelStr

for S1, S2 being full SubRelStr of L st the carrier of S1 = the carrier of S2 holds

RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #)

for S1, S2 being full SubRelStr of L st the carrier of S1 = the carrier of S2 holds

RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #)

proof end;

definition

let L be RelStr ;

let X be Subset of L;

uniqueness

for b_{1}, b_{2} being strict full SubRelStr of L st the carrier of b_{1} = X & the carrier of b_{2} = X holds

b_{1} = b_{2}
by Th57;

existence

ex b_{1} being strict full SubRelStr of L st the carrier of b_{1} = X

end;
let X be Subset of L;

uniqueness

for b

b

existence

ex b

proof end;

:: deftheorem defines subrelstr YELLOW_0:def 15 :

for L being RelStr

for X being Subset of L

for b_{3} being strict full SubRelStr of L holds

( b_{3} = subrelstr X iff the carrier of b_{3} = X );

for L being RelStr

for X being Subset of L

for b

( b

theorem Th58: :: YELLOW_0:58

for L being non empty RelStr

for S being non empty SubRelStr of L

for x being Element of S holds x is Element of L

for S being non empty SubRelStr of L

for x being Element of S holds x is Element of L

proof end;

theorem Th59: :: YELLOW_0:59

for L being RelStr

for S being SubRelStr of L

for a, b being Element of L

for x, y being Element of S st x = a & y = b & x <= y holds

a <= b

for S being SubRelStr of L

for a, b being Element of L

for x, y being Element of S st x = a & y = b & x <= y holds

a <= b

proof end;

theorem Th60: :: YELLOW_0:60

for L being RelStr

for S being full SubRelStr of L

for a, b being Element of L

for x, y being Element of S st x = a & y = b & a <= b & x in the carrier of S holds

x <= y

for S being full SubRelStr of L

for a, b being Element of L

for x, y being Element of S st x = a & y = b & a <= b & x in the carrier of S holds

x <= y

proof end;

theorem Th61: :: YELLOW_0:61

for L being non empty RelStr

for S being non empty full SubRelStr of L

for X being set

for a being Element of L

for x being Element of S st x = a holds

( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) )

for S being non empty full SubRelStr of L

for X being set

for a being Element of L

for x being Element of S st x = a holds

( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) )

proof end;

theorem Th62: :: YELLOW_0:62

for L being non empty RelStr

for S being non empty SubRelStr of L

for X being Subset of S

for a being Element of L

for x being Element of S st x = a holds

( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) )

for S being non empty SubRelStr of L

for X being Subset of S

for a being Element of L

for x being Element of S st x = a holds

( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) )

proof end;

registration

let L be reflexive RelStr ;

coherence

for b_{1} being full SubRelStr of L holds b_{1} is reflexive

end;
coherence

for b

proof end;

registration

let L be transitive RelStr ;

coherence

for b_{1} being full SubRelStr of L holds b_{1} is transitive

end;
coherence

for b

proof end;

registration

let L be antisymmetric RelStr ;

coherence

for b_{1} being full SubRelStr of L holds b_{1} is antisymmetric

end;
coherence

for b

proof end;

definition

let L be non empty RelStr ;

let S be SubRelStr of L;

end;
let S be SubRelStr of L;

attr S is meet-inheriting means :Def16: :: YELLOW_0:def 16

for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L holds

inf {x,y} in the carrier of S;

for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L holds

inf {x,y} in the carrier of S;

:: deftheorem Def16 defines meet-inheriting YELLOW_0:def 16 :

for L being non empty RelStr

for S being SubRelStr of L holds

( S is meet-inheriting iff for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L holds

inf {x,y} in the carrier of S );

for L being non empty RelStr

for S being SubRelStr of L holds

( S is meet-inheriting iff for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L holds

inf {x,y} in the carrier of S );

:: deftheorem Def17 defines join-inheriting YELLOW_0:def 17 :

for L being non empty RelStr

for S being SubRelStr of L holds

( S is join-inheriting iff for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L holds

sup {x,y} in the carrier of S );

for L being non empty RelStr

for S being SubRelStr of L holds

( S is join-inheriting iff for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L holds

sup {x,y} in the carrier of S );

definition

let L be non empty RelStr ;

let S be SubRelStr of L;

end;
let S be SubRelStr of L;

attr S is infs-inheriting means :: YELLOW_0:def 18

for X being Subset of S st ex_inf_of X,L holds

"/\" (X,L) in the carrier of S;

for X being Subset of S st ex_inf_of X,L holds

"/\" (X,L) in the carrier of S;

attr S is sups-inheriting means :: YELLOW_0:def 19

for X being Subset of S st ex_sup_of X,L holds

"\/" (X,L) in the carrier of S;

for X being Subset of S st ex_sup_of X,L holds

"\/" (X,L) in the carrier of S;

:: deftheorem defines infs-inheriting YELLOW_0:def 18 :

for L being non empty RelStr

for S being SubRelStr of L holds

( S is infs-inheriting iff for X being Subset of S st ex_inf_of X,L holds

"/\" (X,L) in the carrier of S );

for L being non empty RelStr

for S being SubRelStr of L holds

( S is infs-inheriting iff for X being Subset of S st ex_inf_of X,L holds

"/\" (X,L) in the carrier of S );

:: deftheorem defines sups-inheriting YELLOW_0:def 19 :

for L being non empty RelStr

for S being SubRelStr of L holds

( S is sups-inheriting iff for X being Subset of S st ex_sup_of X,L holds

"\/" (X,L) in the carrier of S );

for L being non empty RelStr

for S being SubRelStr of L holds

( S is sups-inheriting iff for X being Subset of S st ex_sup_of X,L holds

"\/" (X,L) in the carrier of S );

registration

let L be non empty RelStr ;

coherence

for b_{1} being SubRelStr of L st b_{1} is infs-inheriting holds

b_{1} is meet-inheriting

for b_{1} being SubRelStr of L st b_{1} is sups-inheriting holds

b_{1} is join-inheriting

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let L be non empty RelStr ;

existence

ex b_{1} being SubRelStr of L st

( b_{1} is infs-inheriting & b_{1} is sups-inheriting & not b_{1} is empty & b_{1} is full & b_{1} is strict )

end;
existence

ex b

( b

proof end;

theorem Th63: :: YELLOW_0:63

for L being non empty transitive RelStr

for S being non empty full SubRelStr of L

for X being Subset of S st ex_inf_of X,L & "/\" (X,L) in the carrier of S holds

( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )

for S being non empty full SubRelStr of L

for X being Subset of S st ex_inf_of X,L & "/\" (X,L) in the carrier of S holds

( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )

proof end;

theorem Th64: :: YELLOW_0:64

for L being non empty transitive RelStr

for S being non empty full SubRelStr of L

for X being Subset of S st ex_sup_of X,L & "\/" (X,L) in the carrier of S holds

( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )

for S being non empty full SubRelStr of L

for X being Subset of S st ex_sup_of X,L & "\/" (X,L) in the carrier of S holds

( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )

proof end;

theorem :: YELLOW_0:65

theorem :: YELLOW_0:66

registration

let L be transitive antisymmetric with_infima RelStr ;

for b_{1} being non empty full meet-inheriting SubRelStr of L holds b_{1} is with_infima

end;
cluster non empty full meet-inheriting -> non empty with_infima full meet-inheriting for SubRelStr of L;

coherence for b

proof end;

registration

let L be transitive antisymmetric with_suprema RelStr ;

for b_{1} being non empty full join-inheriting SubRelStr of L holds b_{1} is with_suprema

end;
cluster non empty full join-inheriting -> non empty with_suprema full join-inheriting for SubRelStr of L;

coherence for b

proof end;

theorem :: YELLOW_0:67

for L being non empty complete Poset

for S being non empty full SubRelStr of L

for X being Subset of S st "/\" (X,L) in the carrier of S holds

"/\" (X,S) = "/\" (X,L)

for S being non empty full SubRelStr of L

for X being Subset of S st "/\" (X,L) in the carrier of S holds

"/\" (X,S) = "/\" (X,L)

proof end;

theorem :: YELLOW_0:68

for L being non empty complete Poset

for S being non empty full SubRelStr of L

for X being Subset of S st "\/" (X,L) in the carrier of S holds

"\/" (X,S) = "\/" (X,L)

for S being non empty full SubRelStr of L

for X being Subset of S st "\/" (X,L) in the carrier of S holds

"\/" (X,S) = "\/" (X,L)

proof end;

theorem :: YELLOW_0:69

for L being with_infima Poset

for S being non empty full meet-inheriting SubRelStr of L

for x, y being Element of S

for a, b being Element of L st a = x & b = y holds

x "/\" y = a "/\" b

for S being non empty full meet-inheriting SubRelStr of L

for x, y being Element of S

for a, b being Element of L st a = x & b = y holds

x "/\" y = a "/\" b

proof end;

theorem :: YELLOW_0:70

for L being with_suprema Poset

for S being non empty full join-inheriting SubRelStr of L

for x, y being Element of S

for a, b being Element of L st a = x & b = y holds

x "\/" y = a "\/" b

for S being non empty full join-inheriting SubRelStr of L

for x, y being Element of S

for a, b being Element of L st a = x & b = y holds

x "\/" y = a "\/" b

proof end;