:: Bounds in Posets and Relational Substructures
:: by Grzegorz Bancerek
::
:: Received September 10, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

scheme :: YELLOW_0:sch 1
RelStrEx{ F1() ->  non empty set , P1[ set , set ] } :
 ex L being non empty strict RelStr st
( the carrier of L = F1() & ( for a, b being Element of L holds
( a <= b iff P1[a,b] ) ) )
proofend;

definition
let A be non empty RelStr ;
redefine attr A is reflexive  means :: YELLOW_0:def 1
 for x being Element of A holds x <= x;
compatibility
 ( A is reflexive iff for x being Element of A holds x <= x )
proofend;
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 );

definition
let A be RelStr ;
redefine attr A is transitive  means :: YELLOW_0:def 2
 for x, y, z being Element of A st x <= y &amp; y <= z holds
x <= z;
compatibility
 ( A is transitive iff for x, y, z being Element of A st x <= y &amp; y <= z holds
x <= z )
proofend;
redefine attr A is antisymmetric  means :: YELLOW_0:def 3
 for x, y being Element of A st x <= y &amp; y <= x holds
x = y;
compatibility
 ( A is antisymmetric iff for x, y being Element of A st x <= y &amp; y <= x holds
x = y )
proofend;
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 &amp; 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 &amp; y <= x holds
x = y );

registration
cluster non empty complete  ->  non empty with_suprema with_infima for RelStr ;
coherence
 for b1 being non empty RelStr st b1 is complete holds
( b1 is with_suprema &amp; b1 is with_infima ) by LATTICE3:12;
cluster1 -element reflexive  -> 1 -element reflexive transitive antisymmetric complete for RelStr ;
coherence
 for b1 being 1 -element reflexive RelStr holds
( b1 is complete &amp; b1 is transitive &amp; b1 is antisymmetric )
proofend;
end;

registration
let x be set ;
let R be Relation of {x};
cluster RelStr(# {x},R #) -> 1 -element ;
coherence
 RelStr(# {x},R #) is 1 -element
proofend;
end;

registration
cluster1 -element strict reflexive for RelStr ;
existence
 ex b1 being RelStr st
( b1 is strict &amp; b1 is 1 -element &amp; b1 is reflexive )
proofend;
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 &amp; b1 = b2 holds
( ( a1 <= b1 implies a2 <= b2 ) &amp; ( a1 < b1 implies a2 < b2 ) )
proofend;

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 ) &amp; ( X is_>=_than a1 implies X is_>=_than a2 ) )
proofend;

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 #) &amp; P1 is complete holds
P2 is complete
proofend;

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 ) &amp; ( x is_>=_than X implies y is_>=_than X ) )
proofend;

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 ) &amp; ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) &amp; ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) &amp; ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) )
proofend;

theorem Th6: :: YELLOW_0:6
for L being RelStr
for a being Element of L holds
( {} is_<=_than a &amp; {} is_>=_than a )
proofend;

theorem Th7: :: YELLOW_0:7
for L being RelStr
for a, b being Element of L holds
( ( a is_<=_than {b} implies a <= b ) &amp; ( a <= b implies a is_<=_than {b} ) &amp; ( a is_>=_than {b} implies b <= a ) &amp; ( b <= a implies a is_>=_than {b} ) )
proofend;

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 &amp; a <= c ) ) &amp; ( a <= b &amp; a <= c implies a is_<=_than {b,c} ) &amp; ( a is_>=_than {b,c} implies ( b <= a &amp; c <= a ) ) &amp; ( b <= a &amp; c <= a implies a is_>=_than {b,c} ) )
proofend;

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 ) &amp; ( x is_>=_than Y implies x is_>=_than X ) )
proofend;

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 &amp; x is_<=_than Y implies x is_<=_than X \/ Y ) &amp; ( x is_>=_than X &amp; x is_>=_than Y implies x is_>=_than X \/ Y ) )
proofend;

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 &amp; x <= y holds
X is_<=_than y
proofend;

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 &amp; x >= y holds
X is_>=_than y
proofend;

registration
let L be non empty RelStr ;
cluster [#] L ->  non empty ;
coherence
 not [#] L is empty ;
end;

begin

definition
let L be RelStr ;
attrL is lower-bounded  means :Def4: :: YELLOW_0:def 4
 ex x being Element of L st x is_<=_than the carrier of L;
attrL is upper-bounded  means :Def5: :: YELLOW_0:def 5
 ex x being Element of L st x is_>=_than the carrier of L;
end;

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

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

definition
let L be RelStr ;
attrL is bounded  means :: YELLOW_0:def 6
( L is lower-bounded &amp; L is upper-bounded );
end;

:: deftheorem  defines bounded YELLOW_0:def_6_:_
 for L being RelStr holds
( L is bounded iff ( L is lower-bounded &amp; 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 ) &amp; ( P1 is upper-bounded implies P2 is upper-bounded ) )
proofend;

registration
cluster non empty complete  ->  non empty bounded for RelStr ;
coherence
 for b1 being non empty RelStr st b1 is complete holds
b1 is bounded
proofend;
cluster bounded  ->  lower-bounded upper-bounded for RelStr ;
coherence
 for b1 being RelStr st b1 is bounded holds
( b1 is lower-bounded &amp; b1 is upper-bounded )
proofend;
cluster lower-bounded upper-bounded  ->  bounded for RelStr ;
coherence
 for b1 being RelStr st b1 is lower-bounded &amp; b1 is upper-bounded holds
b1 is bounded
proofend;
end;

registration
cluster non empty V136() reflexive transitive antisymmetric complete for RelStr ;
existence
 ex b1 being non empty Poset st b1 is complete
proofend;
end;

definition
let L be RelStr ;
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 &amp; ( for b being Element of L st X is_<=_than b holds
b >= a ) &amp; ( for c being Element of L st X is_<=_than c &amp; ( 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 &amp; ( for b being Element of L st X is_>=_than b holds
b <= a ) &amp; ( for c being Element of L st X is_>=_than c &amp; ( for b being Element of L st X is_>=_than b holds
b <= c ) holds
c = a ) );
end;

:: 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 &amp; ( for b being Element of L st X is_<=_than b holds
b >= a ) &amp; ( for c being Element of L st X is_<=_than c &amp; ( 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 &amp; ( for b being Element of L st X is_>=_than b holds
b <= a ) &amp; ( for c being Element of L st X is_>=_than c &amp; ( 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 ) &amp; ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) )
proofend;

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 &amp; ( for b being Element of L st X is_<=_than b holds
a <= b ) ) )
proofend;

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 &amp; ( for b being Element of L st X is_>=_than b holds
a >= b ) ) )
proofend;

theorem Th17: :: YELLOW_0:17
for L being non empty antisymmetric complete RelStr
for X being set holds
( ex_sup_of X,L &amp; ex_inf_of X,L )
proofend;

theorem Th18: :: YELLOW_0:18
for L being antisymmetric RelStr
for a, b, c being Element of L holds
( c = a "\/" b &amp; ex_sup_of {a,b},L iff ( c >= a &amp; c >= b &amp; ( for d being Element of L st d >= a &amp; d >= b holds
c <= d ) ) )
proofend;

theorem Th19: :: YELLOW_0:19
for L being antisymmetric RelStr
for a, b, c being Element of L holds
( c = a "/\" b &amp; ex_inf_of {a,b},L iff ( c <= a &amp; c <= b &amp; ( for d being Element of L st d <= a &amp; d <= b holds
c >= d ) ) )
proofend;

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

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

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 &amp; c >= b &amp; ( for d being Element of L st d >= a &amp; d >= b holds
c <= d ) ) )
proofend;

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 &amp; c <= b &amp; ( for d being Element of L st d <= a &amp; d <= b holds
c >= d ) ) )
proofend;

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

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

definition
let L be RelStr ;
let X be set ;
func "\/" (X,L) ->  Element of L means :Def9: :: YELLOW_0:def 9
( X is_<=_than it &amp; ( for a being Element of L st X is_<=_than a holds
it <= a ) ) if  ex_sup_of X,L
;
uniqueness
 for b1, b2 being Element of L st ex_sup_of X,L &amp; X is_<=_than b1 &amp; ( for a being Element of L st X is_<=_than a holds
b1 <= a ) &amp; X is_<=_than b2 &amp; ( for a being Element of L st X is_<=_than a holds
b2 <= a ) holds
b1 = b2
proofend;
existence
 ( ex_sup_of X,L implies ex b1 being Element of L st
( X is_<=_than b1 &amp; ( for a being Element of L st X is_<=_than a holds
b1 <= a ) ) )
proofend;
correctness
consistency
for b1 being Element of L holds verum;
;
func "/\" (X,L) ->  Element of L means :Def10: :: YELLOW_0:def 10
( X is_>=_than it &amp; ( for a being Element of L st X is_>=_than a holds
a <= it ) ) if  ex_inf_of X,L
;
uniqueness
 for b1, b2 being Element of L st ex_inf_of X,L &amp; X is_>=_than b1 &amp; ( for a being Element of L st X is_>=_than a holds
a <= b1 ) &amp; X is_>=_than b2 &amp; ( for a being Element of L st X is_>=_than a holds
a <= b2 ) holds
b1 = b2
proofend;
existence
 ( ex_inf_of X,L implies ex b1 being Element of L st
( X is_>=_than b1 &amp; ( for a being Element of L st X is_>=_than a holds
a <= b1 ) ) )
proofend;
correctness
consistency
for b1 being Element of L holds verum;
;
end;

:: deftheorem Def9 defines "\/" YELLOW_0:def_9_:_
 for L being RelStr
for X being set
for b3 being Element of L st ex_sup_of X,L holds
( b3 = "\/" (X,L) iff ( X is_<=_than b3 &amp; ( for a being Element of L st X is_<=_than a holds
b3 <= a ) ) );

:: deftheorem Def10 defines "/\" YELLOW_0:def_10_:_
 for L being RelStr
for X being set
for b3 being Element of L st ex_inf_of X,L holds
( b3 = "/\" (X,L) iff ( X is_>=_than b3 &amp; ( for a being Element of L st X is_>=_than a holds
a <= b3 ) ) );

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

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

theorem :: YELLOW_0:28
for L being non empty complete Poset
for X being set holds
( "\/" (X,L) = "\/" (X,(latt L)) &amp; "/\" (X,L) = "/\" (X,(latt L)) )
proofend;

theorem :: YELLOW_0:29
for L being complete Lattice
for X being set holds
( "\/" (X,L) = "\/" (X,(LattPOSet L)) &amp; "/\" (X,L) = "/\" (X,(LattPOSet L)) )
proofend;

theorem Th30: :: YELLOW_0:30
for L being antisymmetric RelStr
for a being Element of L
for X being set holds
( a = "\/" (X,L) &amp; ex_sup_of X,L iff ( a is_>=_than X &amp; ( for b being Element of L st b is_>=_than X holds
a <= b ) ) )
proofend;

theorem Th31: :: YELLOW_0:31
for L being antisymmetric RelStr
for a being Element of L
for X being set holds
( a = "/\" (X,L) &amp; ex_inf_of X,L iff ( a is_<=_than X &amp; ( for b being Element of L st b is_<=_than X holds
a >= b ) ) )
proofend;

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 &amp; ( for b being Element of L st b is_>=_than X holds
a <= b ) ) )
proofend;

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 &amp; ( for b being Element of L st b is_<=_than X holds
a >= b ) ) )
proofend;

theorem Th34: :: YELLOW_0:34
for L being RelStr
for X, Y being set st X c= Y &amp; ex_sup_of X,L &amp; ex_sup_of Y,L holds
"\/" (X,L) <= "\/" (Y,L)
proofend;

theorem Th35: :: YELLOW_0:35
for L being RelStr
for X, Y being set st X c= Y &amp; ex_inf_of X,L &amp; ex_inf_of Y,L holds
"/\" (X,L) >= "/\" (Y,L)
proofend;

theorem :: YELLOW_0:36
for L being transitive antisymmetric RelStr
for X, Y being set st ex_sup_of X,L &amp; ex_sup_of Y,L &amp; ex_sup_of X \/ Y,L holds
"\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L))
proofend;

theorem :: YELLOW_0:37
for L being transitive antisymmetric RelStr
for X, Y being set st ex_inf_of X,L &amp; ex_inf_of Y,L &amp; ex_inf_of X \/ Y,L holds
"/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L))
proofend;

notation
let L be RelStr ;
let X be Subset of L;
synonym  sup X for  "\/" (X,L);
synonym  inf X for  "/\" (X,L);
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 &amp; ex_inf_of {a},L )
proofend;

theorem :: YELLOW_0:39
for L being non empty reflexive antisymmetric RelStr
for a being Element of L holds
( sup {a} = a &amp; inf {a} = a )
proofend;

theorem Th40: :: YELLOW_0:40
for L being with_infima Poset
for a, b being Element of L holds inf {a,b} = a "/\" b
proofend;

theorem Th41: :: YELLOW_0:41
for L being with_suprema Poset
for a, b being Element of L holds sup {a,b} = a "\/" b
proofend;

theorem Th42: :: YELLOW_0:42
for L being non empty antisymmetric lower-bounded RelStr holds
( ex_sup_of {} ,L &amp; ex_inf_of the carrier of L,L )
proofend;

theorem Th43: :: YELLOW_0:43
for L being non empty antisymmetric upper-bounded RelStr holds
( ex_inf_of {} ,L &amp; ex_sup_of the carrier of L,L )
proofend;

definition
let L be RelStr ;
func Bottom L ->  Element of L equals :: YELLOW_0:def 11
 "\/" ({},L);
correctness
coherence
"\/" ({},L) is Element of L;
;
func Top L ->  Element of L equals :: YELLOW_0:def 12
 "/\" ({},L);
correctness
coherence
"/\" ({},L) is Element of L;
;
end;

:: deftheorem  defines Bottom YELLOW_0:def_11_:_
 for L being RelStr holds Bottom L = "\/" ({},L);

:: deftheorem  defines Top YELLOW_0:def_12_:_
 for L being RelStr holds Top L = "/\" ({},L);

theorem :: YELLOW_0:44
for L being non empty antisymmetric lower-bounded RelStr
for x being Element of L holds Bottom L <= x
proofend;

theorem :: YELLOW_0:45
for L being non empty antisymmetric upper-bounded RelStr
for x being Element of L holds x <= Top L
proofend;

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 ) ) &amp; ex_sup_of X,L holds
ex_sup_of Y,L
proofend;

theorem Th47: :: YELLOW_0:47
for L being non empty RelStr
for X, Y being set st ex_sup_of X,L &amp; ( for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ) holds
"\/" (X,L) = "\/" (Y,L)
proofend;

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 ) ) &amp; ex_inf_of X,L holds
ex_inf_of Y,L
proofend;

theorem Th49: :: YELLOW_0:49
for L being non empty RelStr
for X, Y being set st ex_inf_of X,L &amp; ( for x being Element of L holds
( x is_<=_than X iff x is_<=_than Y ) ) holds
"/\" (X,L) = "/\" (Y,L)
proofend;

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 ) &amp; ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) &amp; ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) &amp; ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) )
proofend;

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

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

theorem :: YELLOW_0:53
for L being non empty RelStr st ( for X being Subset of L holds ex_sup_of X,L ) holds
L is complete
proofend;

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

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

begin

definition
let L be RelStr ;
mode SubRelStr of L ->  RelStr  means :Def13: :: YELLOW_0:def 13
( the carrier of it c= the carrier of L &amp; the InternalRel of it c= the InternalRel of L );
existence
 ex b1 being RelStr st
( the carrier of b1 c= the carrier of L &amp; the InternalRel of b1 c= the InternalRel of L ) ;
end;

:: deftheorem Def13 defines SubRelStr YELLOW_0:def_13_:_
 for L, b2 being RelStr holds
( b2 is SubRelStr of L iff ( the carrier of b2 c= the carrier of L &amp; the InternalRel of b2 c= the InternalRel of L ) );

definition
let L be RelStr ;
let S be SubRelStr of L;
attrS is full  means :Def14: :: YELLOW_0:def 14
 the InternalRel of S = the InternalRel of L |_2 the carrier of S;
end;

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

registration
let L be RelStr ;
cluster strict full for SubRelStr of L;
existence
 ex b1 being SubRelStr of L st
( b1 is strict &amp; b1 is full )
proofend;
end;

registration
let L be non empty RelStr ;
cluster non empty strict full for SubRelStr of L;
existence
 ex b1 being SubRelStr of L st
( not b1 is empty &amp; b1 is full &amp; b1 is strict )
proofend;
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
proofend;

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

definition
let L be RelStr ;
let X be Subset of L;
func subrelstr X ->  strict full SubRelStr of L means :: YELLOW_0:def 15
 the carrier of it = X;
uniqueness
 for b1, b2 being strict full SubRelStr of L st the carrier of b1 = X &amp; the carrier of b2 = X holds
b1 = b2 by Th57;
existence
 ex b1 being strict full SubRelStr of L st the carrier of b1 = X
proofend;
end;

:: deftheorem  defines subrelstr YELLOW_0:def_15_:_
 for L being RelStr
for X being Subset of L
for b3 being strict full SubRelStr of L holds
( b3 = subrelstr X iff the carrier of b3 = X );

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

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 &amp; y = b &amp; x <= y holds
a <= b
proofend;

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 &amp; y = b &amp; a <= b &amp; x in the carrier of S holds
x <= y
proofend;

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 ) &amp; ( a is_>=_than X implies x is_>=_than X ) )
proofend;

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 ) &amp; ( x is_>=_than X implies a is_>=_than X ) )
proofend;

registration
let L be reflexive RelStr ;
cluster full  ->  reflexive full for SubRelStr of L;
coherence
 for b1 being full SubRelStr of L holds b1 is reflexive
proofend;
end;

registration
let L be transitive RelStr ;
cluster full  ->  transitive full for SubRelStr of L;
coherence
 for b1 being full SubRelStr of L holds b1 is transitive
proofend;
end;

registration
let L be antisymmetric RelStr ;
cluster full  ->  antisymmetric full for SubRelStr of L;
coherence
 for b1 being full SubRelStr of L holds b1 is antisymmetric
proofend;
end;

definition
let L be non empty RelStr ;
let S be SubRelStr of L;
attrS is meet-inheriting  means :Def16: :: YELLOW_0:def 16
 for x, y being Element of L st x in the carrier of S &amp; y in the carrier of S &amp; ex_inf_of {x,y},L holds
inf {x,y} in the carrier of S;
attrS is join-inheriting  means :Def17: :: YELLOW_0:def 17
 for x, y being Element of L st x in the carrier of S &amp; y in the carrier of S &amp; ex_sup_of {x,y},L holds
sup {x,y} in the carrier of S;
end;

:: 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 &amp; y in the carrier of S &amp; 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 &amp; y in the carrier of S &amp; 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;
attrS 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;
attrS 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;
end;

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

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

registration
let L be non empty RelStr ;
cluster infs-inheriting  ->  meet-inheriting for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is infs-inheriting holds
b1 is meet-inheriting
proofend;
cluster sups-inheriting  ->  join-inheriting for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is sups-inheriting holds
b1 is join-inheriting
proofend;
end;

registration
let L be non empty RelStr ;
cluster non empty strict full infs-inheriting sups-inheriting for SubRelStr of L;
existence
 ex b1 being SubRelStr of L st
( b1 is infs-inheriting &amp; b1 is sups-inheriting &amp; not b1 is empty &amp; b1 is full &amp; b1 is strict )
proofend;
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 &amp; "/\" (X,L) in the carrier of S holds
( ex_inf_of X,S &amp; "/\" (X,S) = "/\" (X,L) )
proofend;

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 &amp; "\/" (X,L) in the carrier of S holds
( ex_sup_of X,S &amp; "\/" (X,S) = "\/" (X,L) )
proofend;

theorem :: YELLOW_0:65
for L being non empty transitive RelStr
for S being non empty full SubRelStr of L
for x, y being Element of S st ex_inf_of {x,y},L &amp; "/\" ({x,y},L) in the carrier of S holds
( ex_inf_of {x,y},S &amp; "/\" ({x,y},S) = "/\" ({x,y},L) ) by Th63;

theorem :: YELLOW_0:66
for L being non empty transitive RelStr
for S being non empty full SubRelStr of L
for x, y being Element of S st ex_sup_of {x,y},L &amp; "\/" ({x,y},L) in the carrier of S holds
( ex_sup_of {x,y},S &amp; "\/" ({x,y},S) = "\/" ({x,y},L) ) by Th64;

registration
let L be transitive antisymmetric with_infima RelStr ;
cluster non empty full meet-inheriting  ->  non empty with_infima full meet-inheriting for SubRelStr of L;
coherence
 for b1 being non empty full meet-inheriting SubRelStr of L holds b1 is with_infima
proofend;
end;

registration
let L be transitive antisymmetric with_suprema RelStr ;
cluster non empty full join-inheriting  ->  non empty with_suprema full join-inheriting for SubRelStr of L;
coherence
 for b1 being non empty full join-inheriting SubRelStr of L holds b1 is with_suprema
proofend;
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)
proofend;

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

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 &amp; b = y holds
x "/\" y = a "/\" b
proofend;

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 &amp; b = y holds
x "\/" y = a "\/" b
proofend;