:: YELLOW_0 semantic presentation

scheme :: YELLOW_0:sch 1
s1{ F₁() -> non empty set , P₁[ set , set ] } :

ex b₁ being non empty strict RelStr st
( the carrier of b₁ = F₁() & ( for b₂, b₃ being Element of b₁ holds
( b₂ <= b₃ iff P₁[b₂,b₃] ) ) )

proof end;

definition

let c₁ be non empty RelStr ;
redefine attr a₁ is reflexive means :: YELLOW_0:def 1
for b₁ being Element of a₁ holds b₁ <= b₁;
compatibility

proof end;

end;

:: deftheorem Def1 defines reflexive YELLOW_0:def 1 :

definition

let c₁ be RelStr ;
redefine attr a₁ is transitive means :: YELLOW_0:def 2
for b₁, b₂, b₃ being Element of a₁ st b₁ <= b₂ & b₂ <= b₃ holds
b₁ <= b₃;
compatibility

proof end;

redefine attr a₁ is antisymmetric means :: YELLOW_0:def 3
for b₁, b₂ being Element of a₁ st b₁ <= b₂ & b₂ <= b₁ holds
b₁ = b₂;
compatibility

proof end;

end;

:: deftheorem Def2 defines transitive YELLOW_0:def 2 :

:: deftheorem Def3 defines antisymmetric YELLOW_0:def 3 :

registration

cluster non empty complete -> non empty with_suprema with_infima RelStr ;
coherence by LATTICE3:12;
cluster non empty reflexive trivial -> non empty reflexive transitive antisymmetric complete RelStr ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be Relation of {c₁};
cluster RelStr(# {a₁},a₂ #) -> trivial ;
coherence

proof end;

end;

registration

cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima complete trivial RelStr ;
existence

proof end;

end;

theorem Th1: :: YELLOW_0:1

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₃ = b₅ & b₄ = b₆ holds
( ( b₃ <= b₄ implies b₅ <= b₆ ) & ( b₃ < b₄ implies b₅ < b₆ ) )

proof end;

theorem Th2: :: YELLOW_0:2

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being set
for b₄ being Element of b₁
for b₅ being Element of b₂ st b₄ = b₅ holds
( ( b₃ is_<=_than b₄ implies b₃ is_<=_than b₅ ) & ( b₃ is_>=_than b₄ implies b₃ is_>=_than b₅ ) )

proof end;

theorem Th3: :: YELLOW_0:3

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is complete holds
b₂ is complete

proof end;

theorem Th4: :: YELLOW_0:4

for b₁ being transitive RelStr
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
for b₄ being set holds
( ( b₃ is_<=_than b₄ implies b₂ is_<=_than b₄ ) & ( b₂ is_>=_than b₄ implies b₃ is_>=_than b₄ ) )

proof end;

theorem Th5: :: YELLOW_0:5

for b₁ being non empty RelStr
for b₂ being set
for b₃ being Element of b₁ holds
( ( b₃ is_>=_than b₂ implies b₃ is_>=_than b₂ /\ the carrier of b₁ ) & ( b₃ is_>=_than b₂ /\ the carrier of b₁ implies b₃ is_>=_than b₂ ) & ( b₃ is_<=_than b₂ implies b₃ is_<=_than b₂ /\ the carrier of b₁ ) & ( b₃ is_<=_than b₂ /\ the carrier of b₁ implies b₃ is_<=_than b₂ ) )

proof end;

theorem Th6: :: YELLOW_0:6

for b₁ being RelStr
for b₂ being Element of b₁ holds
( {} is_<=_than b₂ & {} is_>=_than b₂ )

proof end;

theorem Th7: :: YELLOW_0:7

for b₁ being RelStr
for b₂, b₃ being Element of b₁ holds
( ( b₂ is_<=_than {b₃} implies b₂ <= b₃ ) & ( b₂ <= b₃ implies b₂ is_<=_than {b₃} ) & ( b₂ is_>=_than {b₃} implies b₃ <= b₂ ) & ( b₃ <= b₂ implies b₂ is_>=_than {b₃} ) )

proof end;

theorem Th8: :: YELLOW_0:8

for b₁ being RelStr
for b₂, b₃, b₄ being Element of b₁ holds
( ( b₂ is_<=_than {b₃,b₄} implies ( b₂ <= b₃ & b₂ <= b₄ ) ) & ( b₂ <= b₃ & b₂ <= b₄ implies b₂ is_<=_than {b₃,b₄} ) & ( b₂ is_>=_than {b₃,b₄} implies ( b₃ <= b₂ & b₄ <= b₂ ) ) & ( b₃ <= b₂ & b₄ <= b₂ implies b₂ is_>=_than {b₃,b₄} ) )

proof end;

theorem Th9: :: YELLOW_0:9

for b₁ being RelStr
for b₂, b₃ being set st b₂ c= b₃ holds
for b₄ being Element of b₁ holds
( ( b₄ is_<=_than b₃ implies b₄ is_<=_than b₂ ) & ( b₄ is_>=_than b₃ implies b₄ is_>=_than b₂ ) )

proof end;

theorem Th10: :: YELLOW_0:10

for b₁ being RelStr
for b₂, b₃ being set
for b₄ being Element of b₁ holds
( ( b₄ is_<=_than b₂ & b₄ is_<=_than b₃ implies b₄ is_<=_than b₂ \/ b₃ ) & ( b₄ is_>=_than b₂ & b₄ is_>=_than b₃ implies b₄ is_>=_than b₂ \/ b₃ ) )

proof end;

theorem Th11: :: YELLOW_0:11

for b₁ being transitive RelStr
for b₂ being set
for b₃, b₄ being Element of b₁ st b₂ is_<=_than b₃ & b₃ <= b₄ holds
b₂ is_<=_than b₄

proof end;

theorem Th12: :: YELLOW_0:12

for b₁ being transitive RelStr
for b₂ being set
for b₃, b₄ being Element of b₁ st b₂ is_>=_than b₃ & b₃ >= b₄ holds
b₂ is_>=_than b₄

proof end;

registration

let c₁ be non empty RelStr ;
cluster [#] a₁ -> non empty ;
coherence by PRE_TOPC:12;

end;

definition

let c₁ be RelStr ;
attr a₁ is lower-bounded means :Def4: :: YELLOW_0:def 4
ex b₁ being Element of a₁ st b₁ is_<=_than the carrier of a₁;
attr a₁ is upper-bounded means :Def5: :: YELLOW_0:def 5
ex b₁ being Element of a₁ st b₁ is_>=_than the carrier of a₁;

end;

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

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

definition

let c₁ be RelStr ;
attr a₁ is bounded means :: YELLOW_0:def 6
( a₁ is lower-bounded & a₁ is upper-bounded );

end;

:: deftheorem Def6 defines bounded YELLOW_0:def 6 :

theorem Th13: :: YELLOW_0:13

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
( ( b₁ is lower-bounded implies b₂ is lower-bounded ) & ( b₁ is upper-bounded implies b₂ is upper-bounded ) )

proof end;

registration

cluster non empty complete -> non empty bounded RelStr ;
coherence

proof end;

cluster bounded -> lower-bounded upper-bounded RelStr ;
coherence

proof end;

cluster lower-bounded upper-bounded -> bounded RelStr ;
coherence

proof end;

end;

registration

cluster non empty with_suprema with_infima complete lower-bounded upper-bounded bounded RelStr ;
existence

proof end;

end;

definition

let c₁ be RelStr ;
let c₂ be set ;
pred ex_sup_of c₂,c₁ means :Def7: :: YELLOW_0:def 7
ex b₁ being Element of a₁ st
( a₂ is_<=_than b₁ & ( for b₂ being Element of a₁ st a₂ is_<=_than b₂ holds
b₂ >= b₁ ) & ( for b₂ being Element of a₁ st a₂ is_<=_than b₂ & ( for b₃ being Element of a₁ st a₂ is_<=_than b₃ holds
b₃ >= b₂ ) holds
b₂ = b₁ ) );
pred ex_inf_of c₂,c₁ means :Def8: :: YELLOW_0:def 8
ex b₁ being Element of a₁ st
( a₂ is_>=_than b₁ & ( for b₂ being Element of a₁ st a₂ is_>=_than b₂ holds
b₂ <= b₁ ) & ( for b₂ being Element of a₁ st a₂ is_>=_than b₂ & ( for b₃ being Element of a₁ st a₂ is_>=_than b₃ holds
b₃ <= b₂ ) holds
b₂ = b₁ ) );

end;

:: deftheorem Def7 defines ex_sup_of YELLOW_0:def 7 :

:: deftheorem Def8 defines ex_inf_of YELLOW_0:def 8 :

theorem Th14: :: YELLOW_0:14

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being set holds
( ( ex_sup_of b₃,b₁ implies ex_sup_of b₃,b₂ ) & ( ex_inf_of b₃,b₁ implies ex_inf_of b₃,b₂ ) )

proof end;

theorem Th15: :: YELLOW_0:15

for b₁ being antisymmetric RelStr
for b₂ being set holds
( ex_sup_of b₂,b₁ iff ex b₃ being Element of b₁ st
( b₂ is_<=_than b₃ & ( for b₄ being Element of b₁ st b₂ is_<=_than b₄ holds
b₃ <= b₄ ) ) )

proof end;

theorem Th16: :: YELLOW_0:16

for b₁ being antisymmetric RelStr
for b₂ being set holds
( ex_inf_of b₂,b₁ iff ex b₃ being Element of b₁ st
( b₂ is_>=_than b₃ & ( for b₄ being Element of b₁ st b₂ is_>=_than b₄ holds
b₃ >= b₄ ) ) )

proof end;

theorem Th17: :: YELLOW_0:17

for b₁ being non empty antisymmetric complete RelStr
for b₂ being set holds
( ex_sup_of b₂,b₁ & ex_inf_of b₂,b₁ )

proof end;

theorem Th18: :: YELLOW_0:18

for b₁ being antisymmetric RelStr
for b₂, b₃, b₄ being Element of b₁ holds
( b₄ = b₂ "\/" b₃ & ex_sup_of {b₂,b₃},b₁ iff ( b₄ >= b₂ & b₄ >= b₃ & ( for b₅ being Element of b₁ st b₅ >= b₂ & b₅ >= b₃ holds
b₄ <= b₅ ) ) )

proof end;

theorem Th19: :: YELLOW_0:19

for b₁ being antisymmetric RelStr
for b₂, b₃, b₄ being Element of b₁ holds
( b₄ = b₂ "/\" b₃ & ex_inf_of {b₂,b₃},b₁ iff ( b₄ <= b₂ & b₄ <= b₃ & ( for b₅ being Element of b₁ st b₅ <= b₂ & b₅ <= b₃ holds
b₄ >= b₅ ) ) )

proof end;

theorem Th20: :: YELLOW_0:20

for b₁ being antisymmetric RelStr holds
( b₁ is with_suprema iff for b₂, b₃ being Element of b₁ holds ex_sup_of {b₂,b₃},b₁ )

proof end;

theorem Th21: :: YELLOW_0:21

for b₁ being antisymmetric RelStr holds
( b₁ is with_infima iff for b₂, b₃ being Element of b₁ holds ex_inf_of {b₂,b₃},b₁ )

proof end;

theorem Th22: :: YELLOW_0:22

for b₁ being antisymmetric with_suprema RelStr
for b₂, b₃, b₄ being Element of b₁ holds
( b₄ = b₂ "\/" b₃ iff ( b₄ >= b₂ & b₄ >= b₃ & ( for b₅ being Element of b₁ st b₅ >= b₂ & b₅ >= b₃ holds
b₄ <= b₅ ) ) )

proof end;

theorem Th23: :: YELLOW_0:23

for b₁ being antisymmetric with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ holds
( b₄ = b₂ "/\" b₃ iff ( b₄ <= b₂ & b₄ <= b₃ & ( for b₅ being Element of b₁ st b₅ <= b₂ & b₅ <= b₃ holds
b₄ >= b₅ ) ) )

proof end;

theorem Th24: :: YELLOW_0:24

for b₁ being reflexive antisymmetric with_suprema RelStr
for b₂, b₃ being Element of b₁ holds
( b₂ = b₂ "\/" b₃ iff b₂ >= b₃ )

proof end;

theorem Th25: :: YELLOW_0:25

for b₁ being reflexive antisymmetric with_infima RelStr
for b₂, b₃ being Element of b₁ holds
( b₂ = b₂ "/\" b₃ iff b₂ <= b₃ )

proof end;

definition

let c₁ be RelStr ;
let c₂ be set ;
func "\/" c₂,c₁ -> Element of a₁ means :Def9: :: YELLOW_0:def 9
( a₂ is_<=_than a₃ & ( for b₁ being Element of a₁ st a₂ is_<=_than b₁ holds
a₃ <= b₁ ) ) if ex_sup_of a₂,a₁
;
uniqueness

proof end;

existence

proof end;

correctness ;
func "/\" c₂,c₁ -> Element of a₁ means :Def10: :: YELLOW_0:def 10
( a₂ is_>=_than a₃ & ( for b₁ being Element of a₁ st a₂ is_>=_than b₁ holds
b₁ <= a₃ ) ) if ex_inf_of a₂,a₁
;
uniqueness

proof end;

existence

proof end;

correctness ;

end;

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

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

theorem Th26: :: YELLOW_0:26

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being set st ex_sup_of b₃,b₁ holds
"\/" b₃,b₁ = "\/" b₃,b₂

proof end;

theorem Th27: :: YELLOW_0:27

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being set st ex_inf_of b₃,b₁ holds
"/\" b₃,b₁ = "/\" b₃,b₂

proof end;

theorem Th28: :: YELLOW_0:28

for b₁ being non empty complete Poset
for b₂ being set holds
( "\/" b₂,b₁ = "\/" b₂,(latt b₁) & "/\" b₂,b₁ = "/\" b₂,(latt b₁) )

proof end;

theorem Th29: :: YELLOW_0:29

for b₁ being complete Lattice
for b₂ being set holds
( "\/" b₂,b₁ = "\/" b₂,(LattPOSet b₁) & "/\" b₂,b₁ = "/\" b₂,(LattPOSet b₁) )

proof end;

theorem Th30: :: YELLOW_0:30

for b₁ being antisymmetric RelStr
for b₂ being Element of b₁
for b₃ being set holds
( b₂ = "\/" b₃,b₁ & ex_sup_of b₃,b₁ iff ( b₂ is_>=_than b₃ & ( for b₄ being Element of b₁ st b₄ is_>=_than b₃ holds
b₂ <= b₄ ) ) )

proof end;

theorem Th31: :: YELLOW_0:31

for b₁ being antisymmetric RelStr
for b₂ being Element of b₁
for b₃ being set holds
( b₂ = "/\" b₃,b₁ & ex_inf_of b₃,b₁ iff ( b₂ is_<=_than b₃ & ( for b₄ being Element of b₁ st b₄ is_<=_than b₃ holds
b₂ >= b₄ ) ) )

proof end;

theorem Th32: :: YELLOW_0:32

for b₁ being non empty antisymmetric complete RelStr
for b₂ being Element of b₁
for b₃ being set holds
( b₂ = "\/" b₃,b₁ iff ( b₂ is_>=_than b₃ & ( for b₄ being Element of b₁ st b₄ is_>=_than b₃ holds
b₂ <= b₄ ) ) )

proof end;

theorem Th33: :: YELLOW_0:33

for b₁ being non empty antisymmetric complete RelStr
for b₂ being Element of b₁
for b₃ being set holds
( b₂ = "/\" b₃,b₁ iff ( b₂ is_<=_than b₃ & ( for b₄ being Element of b₁ st b₄ is_<=_than b₃ holds
b₂ >= b₄ ) ) )

proof end;

theorem Th34: :: YELLOW_0:34

for b₁ being RelStr
for b₂, b₃ being set st b₂ c= b₃ & ex_sup_of b₂,b₁ & ex_sup_of b₃,b₁ holds
"\/" b₂,b₁ <= "\/" b₃,b₁

proof end;

theorem Th35: :: YELLOW_0:35

for b₁ being RelStr
for b₂, b₃ being set st b₂ c= b₃ & ex_inf_of b₂,b₁ & ex_inf_of b₃,b₁ holds
"/\" b₂,b₁ >= "/\" b₃,b₁

proof end;

theorem Th36: :: YELLOW_0:36

for b₁ being transitive antisymmetric RelStr
for b₂, b₃ being set st ex_sup_of b₂,b₁ & ex_sup_of b₃,b₁ & ex_sup_of b₂ \/ b₃,b₁ holds
"\/" (b₂ \/ b₃),b₁ = ("\/" b₂,b₁) "\/" ("\/" b₃,b₁)

proof end;

theorem Th37: :: YELLOW_0:37

for b₁ being transitive antisymmetric RelStr
for b₂, b₃ being set st ex_inf_of b₂,b₁ & ex_inf_of b₃,b₁ & ex_inf_of b₂ \/ b₃,b₁ holds
"/\" (b₂ \/ b₃),b₁ = ("/\" b₂,b₁) "/\" ("/\" b₃,b₁)

proof end;

notation

let c₁ be RelStr ;
let c₂ be Subset of c₁;
synonym sup c₂ for "\/" c₂,c₁;
synonym inf c₂ for "/\" c₂,c₁;

end;

theorem Th38: :: YELLOW_0:38

for b₁ being non empty reflexive antisymmetric RelStr
for b₂ being Element of b₁ holds
( ex_sup_of {b₂},b₁ & ex_inf_of {b₂},b₁ )

proof end;

theorem Th39: :: YELLOW_0:39

for b₁ being non empty reflexive antisymmetric RelStr
for b₂ being Element of b₁ holds
( sup {b₂} = b₂ & inf {b₂} = b₂ )

proof end;

theorem Th40: :: YELLOW_0:40

for b₁ being with_infima Poset
for b₂, b₃ being Element of b₁ holds inf {b₂,b₃} = b₂ "/\" b₃

proof end;

theorem Th41: :: YELLOW_0:41

for b₁ being with_suprema Poset
for b₂, b₃ being Element of b₁ holds sup {b₂,b₃} = b₂ "\/" b₃

proof end;

theorem Th42: :: YELLOW_0:42

for b₁ being non empty antisymmetric lower-bounded RelStr holds
( ex_sup_of {} ,b₁ & ex_inf_of the carrier of b₁,b₁ )

proof end;

theorem Th43: :: YELLOW_0:43

for b₁ being non empty antisymmetric upper-bounded RelStr holds
( ex_inf_of {} ,b₁ & ex_sup_of the carrier of b₁,b₁ )

proof end;

definition

let c₁ be RelStr ;
func Bottom c₁ -> Element of a₁ equals :: YELLOW_0:def 11
"\/" {} ,a₁;
correctness ;
func Top c₁ -> Element of a₁ equals :: YELLOW_0:def 12
"/\" {} ,a₁;
correctness ;

end;

:: deftheorem Def11 defines Bottom YELLOW_0:def 11 :

:: deftheorem Def12 defines Top YELLOW_0:def 12 :

theorem Th44: :: YELLOW_0:44

for b₁ being non empty antisymmetric lower-bounded RelStr
for b₂ being Element of b₁ holds Bottom b₁ <= b₂

proof end;

theorem Th45: :: YELLOW_0:45

for b₁ being non empty antisymmetric upper-bounded RelStr
for b₂ being Element of b₁ holds b₂ <= Top b₁

proof end;

theorem Th46: :: YELLOW_0:46

for b₁ being non empty RelStr
for b₂, b₃ being set st ( for b₄ being Element of b₁ holds
( b₄ is_>=_than b₂ iff b₄ is_>=_than b₃ ) ) & ex_sup_of b₂,b₁ holds
ex_sup_of b₃,b₁

proof end;

theorem Th47: :: YELLOW_0:47

for b₁ being non empty RelStr
for b₂, b₃ being set st ex_sup_of b₂,b₁ & ( for b₄ being Element of b₁ holds
( b₄ is_>=_than b₂ iff b₄ is_>=_than b₃ ) ) holds
"\/" b₂,b₁ = "\/" b₃,b₁

proof end;

theorem Th48: :: YELLOW_0:48

for b₁ being non empty RelStr
for b₂, b₃ being set st ( for b₄ being Element of b₁ holds
( b₄ is_<=_than b₂ iff b₄ is_<=_than b₃ ) ) & ex_inf_of b₂,b₁ holds
ex_inf_of b₃,b₁

proof end;

theorem Th49: :: YELLOW_0:49

for b₁ being non empty RelStr
for b₂, b₃ being set st ex_inf_of b₂,b₁ & ( for b₄ being Element of b₁ holds
( b₄ is_<=_than b₂ iff b₄ is_<=_than b₃ ) ) holds
"/\" b₂,b₁ = "/\" b₃,b₁

proof end;

theorem Th50: :: YELLOW_0:50

for b₁ being non empty RelStr
for b₂ being set holds
( ( ex_sup_of b₂,b₁ implies ex_sup_of b₂ /\ the carrier of b₁,b₁ ) & ( ex_sup_of b₂ /\ the carrier of b₁,b₁ implies ex_sup_of b₂,b₁ ) & ( ex_inf_of b₂,b₁ implies ex_inf_of b₂ /\ the carrier of b₁,b₁ ) & ( ex_inf_of b₂ /\ the carrier of b₁,b₁ implies ex_inf_of b₂,b₁ ) )

proof end;

theorem Th51: :: YELLOW_0:51

for b₁ being non empty RelStr
for b₂ being set st ( ex_sup_of b₂,b₁ or ex_sup_of b₂ /\ the carrier of b₁,b₁ ) holds
"\/" b₂,b₁ = "\/" (b₂ /\ the carrier of b₁),b₁

proof end;

theorem Th52: :: YELLOW_0:52

for b₁ being non empty RelStr
for b₂ being set st ( ex_inf_of b₂,b₁ or ex_inf_of b₂ /\ the carrier of b₁,b₁ ) holds
"/\" b₂,b₁ = "/\" (b₂ /\ the carrier of b₁),b₁

proof end;

theorem Th53: :: YELLOW_0:53

for b₁ being non empty RelStr st ( for b₂ being Subset of b₁ holds ex_sup_of b₂,b₁ ) holds
b₁ is complete

proof end;

theorem Th54: :: YELLOW_0:54

for b₁ being non empty Poset holds
( b₁ is with_suprema iff for b₂ being non empty finite Subset of b₁ holds ex_sup_of b₂,b₁ )

proof end;

theorem Th55: :: YELLOW_0:55

for b₁ being non empty Poset holds
( b₁ is with_infima iff for b₂ being non empty finite Subset of b₁ holds ex_inf_of b₂,b₁ )

proof end;

theorem Th56: :: YELLOW_0:56

for b₁ being set
for b₂ being Relation of b₁ holds b₂ = b₂ |_2 b₁

proof end;

definition

let c₁ be RelStr ;
mode SubRelStr of c₁ -> RelStr means :Def13: :: YELLOW_0:def 13
( the carrier of a₂ c= the carrier of a₁ & the InternalRel of a₂ c= the InternalRel of a₁ );
existence ;

end;

:: deftheorem Def13 defines SubRelStr YELLOW_0:def 13 :

definition

let c₁ be RelStr ;
let c₂ be SubRelStr of c₁;
attr a₂ is full means :Def14: :: YELLOW_0:def 14
the InternalRel of a₂ = the InternalRel of a₁ |_2 the carrier of a₂;

end;

:: deftheorem Def14 defines full YELLOW_0:def 14 :

registration

let c₁ be RelStr ;
cluster strict full SubRelStr of a₁;
existence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster non empty strict full SubRelStr of a₁;
existence

proof end;

end;

theorem Th57: :: YELLOW_0:57

for b₁ being RelStr
for b₂ being Subset of b₁ holds RelStr(# b₂,(the InternalRel of b₁ |_2 b₂) #) is full SubRelStr of b₁

proof end;

theorem Th58: :: YELLOW_0:58

for b₁ being RelStr
for b₂, b₃ being full SubRelStr of b₁ st the carrier of b₂ = the carrier of b₃ holds
RelStr(# the carrier of b₂,the InternalRel of b₂ #) = RelStr(# the carrier of b₃,the InternalRel of b₃ #)

proof end;

definition

let c₁ be RelStr ;
let c₂ be Subset of c₁;
func subrelstr c₂ -> strict full SubRelStr of a₁ means :: YELLOW_0:def 15
the carrier of a₃ = a₂;
uniqueness by Th58;
existence

proof end;

end;

:: deftheorem Def15 defines subrelstr YELLOW_0:def 15 :

theorem Th59: :: YELLOW_0:59

for b₁ being non empty RelStr
for b₂ being non empty SubRelStr of b₁
for b₃ being Element of b₂ holds b₃ is Element of b₁

proof end;

theorem Th60: :: YELLOW_0:60

for b₁ being RelStr
for b₂ being SubRelStr of b₁
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₅ = b₃ & b₆ = b₄ & b₅ <= b₆ holds
b₃ <= b₄

proof end;

theorem Th61: :: YELLOW_0:61

for b₁ being RelStr
for b₂ being full SubRelStr of b₁
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₅ = b₃ & b₆ = b₄ & b₃ <= b₄ & b₅ in the carrier of b₂ & b₆ in the carrier of b₂ holds
b₅ <= b₆

proof end;

theorem Th62: :: YELLOW_0:62

for b₁ being non empty RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃ being set
for b₄ being Element of b₁
for b₅ being Element of b₂ st b₅ = b₄ holds
( ( b₄ is_<=_than b₃ implies b₅ is_<=_than b₃ ) & ( b₄ is_>=_than b₃ implies b₅ is_>=_than b₃ ) )

proof end;

theorem Th63: :: YELLOW_0:63

for b₁ being non empty RelStr
for b₂ being non empty SubRelStr of b₁
for b₃ being Subset of b₂
for b₄ being Element of b₁
for b₅ being Element of b₂ st b₅ = b₄ holds
( ( b₅ is_<=_than b₃ implies b₄ is_<=_than b₃ ) & ( b₅ is_>=_than b₃ implies b₄ is_>=_than b₃ ) )

proof end;

registration

let c₁ be reflexive RelStr ;
cluster full -> reflexive full SubRelStr of a₁;
coherence

proof end;

end;

registration

let c₁ be transitive RelStr ;
cluster full -> transitive full SubRelStr of a₁;
coherence

proof end;

end;

registration

let c₁ be antisymmetric RelStr ;
cluster full -> antisymmetric full SubRelStr of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be SubRelStr of c₁;
attr a₂ is meet-inheriting means :Def16: :: YELLOW_0:def 16
for b₁, b₂ being Element of a₁ st b₁ in the carrier of a₂ & b₂ in the carrier of a₂ & ex_inf_of {b₁,b₂},a₁ holds
inf {b₁,b₂} in the carrier of a₂;
attr a₂ is join-inheriting means :Def17: :: YELLOW_0:def 17
for b₁, b₂ being Element of a₁ st b₁ in the carrier of a₂ & b₂ in the carrier of a₂ & ex_sup_of {b₁,b₂},a₁ holds
sup {b₁,b₂} in the carrier of a₂;

end;

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

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

definition

let c₁ be non empty RelStr ;
let c₂ be SubRelStr of c₁;
attr a₂ is infs-inheriting means :: YELLOW_0:def 18
for b₁ being Subset of a₂ st ex_inf_of b₁,a₁ holds
"/\" b₁,a₁ in the carrier of a₂;
attr a₂ is sups-inheriting means :: YELLOW_0:def 19
for b₁ being Subset of a₂ st ex_sup_of b₁,a₁ holds
"\/" b₁,a₁ in the carrier of a₂;

end;

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

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

registration

let c₁ be non empty RelStr ;
cluster infs-inheriting -> meet-inheriting SubRelStr of a₁;
coherence

proof end;

cluster sups-inheriting -> join-inheriting SubRelStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster non empty strict full meet-inheriting join-inheriting infs-inheriting sups-inheriting SubRelStr of a₁;
existence

proof end;

end;

theorem Th64: :: YELLOW_0:64

for b₁ being non empty transitive RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃ being Subset of b₂ st ex_inf_of b₃,b₁ & "/\" b₃,b₁ in the carrier of b₂ holds
( ex_inf_of b₃,b₂ & "/\" b₃,b₂ = "/\" b₃,b₁ )

proof end;

theorem Th65: :: YELLOW_0:65

for b₁ being non empty transitive RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃ being Subset of b₂ st ex_sup_of b₃,b₁ & "\/" b₃,b₁ in the carrier of b₂ holds
( ex_sup_of b₃,b₂ & "\/" b₃,b₂ = "\/" b₃,b₁ )

proof end;

theorem Th66: :: YELLOW_0:66

for b₁ being non empty transitive RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃, b₄ being Element of b₂ st ex_inf_of {b₃,b₄},b₁ & "/\" {b₃,b₄},b₁ in the carrier of b₂ holds
( ex_inf_of {b₃,b₄},b₂ & "/\" {b₃,b₄},b₂ = "/\" {b₃,b₄},b₁ ) by Th64;

theorem Th67: :: YELLOW_0:67

for b₁ being non empty transitive RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃, b₄ being Element of b₂ st ex_sup_of {b₃,b₄},b₁ & "\/" {b₃,b₄},b₁ in the carrier of b₂ holds
( ex_sup_of {b₃,b₄},b₂ & "\/" {b₃,b₄},b₂ = "\/" {b₃,b₄},b₁ ) by Th65;

registration

let c₁ be transitive antisymmetric with_infima RelStr ;
cluster non empty full meet-inheriting -> non empty transitive antisymmetric with_infima full meet-inheriting SubRelStr of a₁;
coherence

proof end;

end;

registration

let c₁ be transitive antisymmetric with_suprema RelStr ;
cluster non empty full join-inheriting -> non empty transitive antisymmetric with_suprema full join-inheriting SubRelStr of a₁;
coherence

proof end;

end;

theorem Th68: :: YELLOW_0:68

for b₁ being non empty complete Poset
for b₂ being non empty full SubRelStr of b₁
for b₃ being Subset of b₂ st "/\" b₃,b₁ in the carrier of b₂ holds
"/\" b₃,b₂ = "/\" b₃,b₁

proof end;

theorem Th69: :: YELLOW_0:69

for b₁ being non empty complete Poset
for b₂ being non empty full SubRelStr of b₁
for b₃ being Subset of b₂ st "\/" b₃,b₁ in the carrier of b₂ holds
"\/" b₃,b₂ = "\/" b₃,b₁

proof end;

theorem Th70: :: YELLOW_0:70

for b₁ being with_infima Poset
for b₂ being non empty full meet-inheriting SubRelStr of b₁
for b₃, b₄ being Element of b₂
for b₅, b₆ being Element of b₁ st b₅ = b₃ & b₆ = b₄ holds
b₃ "/\" b₄ = b₅ "/\" b₆

proof end;

theorem Th71: :: YELLOW_0:71

for b₁ being with_suprema Poset
for b₂ being non empty full join-inheriting SubRelStr of b₁
for b₃, b₄ being Element of b₂
for b₅, b₆ being Element of b₁ st b₅ = b₃ & b₆ = b₄ holds
b₃ "\/" b₄ = b₅ "\/" b₆

proof end;