:: YELLOW11 semantic presentation
begin
theorem
:: YELLOW11:1
3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
=
{
0
: ( ( ) (
empty
V27
()
V28
()
V29
()
V31
()
V32
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ,1 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ,2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
}
: ( ( ) ( non
empty
)
Element
of
K32
(
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: YELLOW11:2
2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
\
1 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
K32
(2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ) : ( ( ) ( non
empty
)
set
) )
=
{
1 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
}
: ( ( ) ( non
empty
)
Element
of
K32
(
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: YELLOW11:3
3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
\
1 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
K32
(3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ) : ( ( ) ( non
empty
)
set
) )
=
{
1 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ,2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
}
: ( ( ) ( non
empty
)
Element
of
K32
(
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: YELLOW11:4
3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
\
2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
K32
(3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ) : ( ( ) ( non
empty
)
set
) )
=
{
2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
}
: ( ( ) ( non
empty
)
Element
of
K32
(
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
)
set
) ) ;
begin
theorem
:: YELLOW11:5
for
L
being ( (
reflexive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
antisymmetric
with_suprema
with_infima
)
RelStr
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
antisymmetric
with_suprema
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) iff
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
antisymmetric
with_suprema
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: YELLOW11:6
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
)
for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
"\/"
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
<=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: YELLOW11:7
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
)
for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
<=
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
"/\"
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: YELLOW11:8
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
)
for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
<=
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
"/\"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) ;
definition
func
N_5
->
( ( ) ( )
RelStr
)
equals
:: YELLOW11:def 1
InclPoset
{
0
: ( ( ) (
empty
V27
()
V28
()
V29
()
V31
()
V32
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ,
(
3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
\
1 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) ( )
Element
of
K32
(3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ) : ( ( ) ( non
empty
)
set
) ) ,2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ,
(
3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
\
2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) ( )
Element
of
K32
(3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ) : ( ( ) ( non
empty
)
set
) ) ,3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
}
: ( ( ) ( non
empty
)
set
) : ( (
strict
) ( non
empty
strict
V58
()
reflexive
transitive
antisymmetric
)
RelStr
) ;
end;
registration
cluster
N_5
: ( ( ) ( )
RelStr
)
->
strict
reflexive
transitive
antisymmetric
;
cluster
N_5
: ( ( ) ( )
RelStr
)
->
with_suprema
with_infima
;
end;
definition
func
M_3
->
( ( ) ( )
RelStr
)
equals
:: YELLOW11:def 2
InclPoset
{
0
: ( ( ) (
empty
V27
()
V28
()
V29
()
V31
()
V32
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ,1 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ,
(
2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
\
1 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) ( )
Element
of
K32
(2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ) : ( ( ) ( non
empty
)
set
) ) ,
(
3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
\
2 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) ( )
Element
of
K32
(3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ) : ( ( ) ( non
empty
)
set
) ) ,3 : ( ( ) ( non
empty
V18
()
V27
()
V28
()
V29
()
V33
() )
Element
of
NAT
: ( ( ) ( non
empty
V27
()
V28
()
V29
() )
Element
of
K32
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
}
: ( ( ) ( non
empty
)
set
) : ( (
strict
) ( non
empty
strict
V58
()
reflexive
transitive
antisymmetric
)
RelStr
) ;
end;
registration
cluster
M_3
: ( ( ) ( )
RelStr
)
->
strict
reflexive
transitive
antisymmetric
;
cluster
M_3
: ( ( ) ( )
RelStr
)
->
with_suprema
with_infima
;
end;
theorem
:: YELLOW11:9
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) holds
( ex
K
being ( (
full
meet-inheriting
join-inheriting
) (
V58
()
reflexive
transitive
antisymmetric
full
meet-inheriting
join-inheriting
)
Sublattice
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) ) st
N_5
: ( ( ) ( non
empty
strict
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
RelStr
) ,
K
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
are_isomorphic
iff ex
a
,
b
,
c
,
d
,
e
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: YELLOW11:10
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) holds
( ex
K
being ( (
full
meet-inheriting
join-inheriting
) (
V58
()
reflexive
transitive
antisymmetric
full
meet-inheriting
join-inheriting
)
Sublattice
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) ) st
M_3
: ( ( ) ( non
empty
strict
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
RelStr
) ,
K
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
are_isomorphic
iff ex
a
,
b
,
c
,
d
,
e
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
d
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
=
e
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;
begin
definition
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
attr
L
is
modular
means
:: YELLOW11:def 3
for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
L
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of the
carrier
of
L
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
L
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
"/\"
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
L
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
registration
cluster
non
empty
reflexive
antisymmetric
with_infima
distributive
->
non
empty
reflexive
antisymmetric
with_infima
modular
for ( ( ) ( )
RelStr
) ;
end;
theorem
:: YELLOW11:11
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) holds
(
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) is
modular
iff for
K
being ( (
full
meet-inheriting
join-inheriting
) (
V58
()
reflexive
transitive
antisymmetric
full
meet-inheriting
join-inheriting
)
Sublattice
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) ) holds not
N_5
: ( ( ) ( non
empty
strict
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
RelStr
) ,
K
: ( (
full
meet-inheriting
join-inheriting
) (
V58
()
reflexive
transitive
antisymmetric
full
meet-inheriting
join-inheriting
)
Sublattice
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) )
are_isomorphic
) ;
theorem
:: YELLOW11:12
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) st
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) is
modular
holds
(
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) is
distributive
iff for
K
being ( (
full
meet-inheriting
join-inheriting
) (
V58
()
reflexive
transitive
antisymmetric
full
meet-inheriting
join-inheriting
)
Sublattice
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) ) holds not
M_3
: ( ( ) ( non
empty
strict
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
RelStr
) ,
K
: ( (
full
meet-inheriting
join-inheriting
) (
V58
()
reflexive
transitive
antisymmetric
full
meet-inheriting
join-inheriting
)
Sublattice
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) )
are_isomorphic
) ;
begin
definition
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
let
a
,
b
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
func
[#
a
,
b
#]
->
( ( ) ( )
Subset
of )
means
:: YELLOW11:def 4
for
c
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
(
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
it
: ( (
Function-like
V21
(
a
: ( ( ) ( )
set
) , the
carrier
of
L
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) (
V7
()
V10
(
a
: ( ( ) ( )
set
) )
V11
( the
carrier
of
L
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
Function-like
V21
(
a
: ( ( ) ( )
set
) , the
carrier
of
L
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Element
of
K32
(
K33
(
a
: ( ( ) ( )
set
) , the
carrier
of
L
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) iff (
a
: ( ( ) ( )
set
)
<=
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
b
: ( ( ) (
V7
()
V10
(
a
: ( ( ) ( )
set
) )
V11
(
a
: ( ( ) ( )
set
) ) )
Element
of
K32
(
K33
(
a
: ( ( ) ( )
set
) ,
a
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) );
end;
definition
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
let
IT
be ( ( ) ( )
Subset
of ) ;
attr
IT
is
interval
means
:: YELLOW11:def 5
ex
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
IT
: ( ( ) ( )
set
)
=
[#
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ,
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
#]
: ( ( ) ( )
Subset
of ) ;
end;
registration
let
L
be ( ( non
empty
reflexive
transitive
) ( non
empty
V58
()
reflexive
transitive
)
RelStr
) ;
cluster
non
empty
interval
->
directed
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
non
empty
interval
->
filtered
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
let
a
,
b
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
[#
a
: ( ( ) ( )
Element
of the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ,
b
: ( ( ) ( )
Element
of the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
#]
: ( ( ) ( )
Subset
of )
->
interval
;
end;
theorem
:: YELLOW11:13
for
L
being ( ( non
empty
reflexive
transitive
) ( non
empty
V58
()
reflexive
transitive
)
RelStr
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
[#
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ,
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
#]
: ( ( ) (
interval
)
Subset
of )
=
(
uparrow
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
V58
()
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
/\
(
downarrow
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
V58
()
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
V58
()
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_infima
)
Poset
) ;
let
a
,
b
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
subrelstr
[#
a
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ,
b
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
#]
: ( ( ) (
interval
)
Subset
of ) : ( (
strict
full
) (
strict
V58
()
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_infima
)
RelStr
) )
->
strict
full
meet-inheriting
;
end;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
)
Poset
) ;
let
a
,
b
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
subrelstr
[#
a
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ,
b
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
#]
: ( ( ) (
interval
)
Subset
of ) : ( (
strict
full
) (
strict
V58
()
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) )
->
strict
full
join-inheriting
;
end;
theorem
:: YELLOW11:14
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) is
modular
holds
subrelstr
[#
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ,
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
#]
: ( ( ) (
interval
)
Subset
of ) : ( (
strict
full
) (
strict
V58
()
reflexive
transitive
antisymmetric
full
meet-inheriting
join-inheriting
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) ) ,
subrelstr
[#
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) ,
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
#]
: ( ( ) (
interval
)
Subset
of ) : ( (
strict
full
) (
strict
V58
()
reflexive
transitive
antisymmetric
full
meet-inheriting
join-inheriting
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
with_infima
) ( non
empty
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
)
LATTICE
) )
are_isomorphic
;
registration
cluster
non
empty
finite
V58
()
reflexive
transitive
antisymmetric
with_suprema
with_infima
for ( ( ) ( )
RelStr
) ;
end;
registration
cluster
finite
reflexive
transitive
antisymmetric
with_infima
->
reflexive
transitive
antisymmetric
with_infima
lower-bounded
for ( ( ) ( )
RelStr
) ;
end;
registration
cluster
finite
reflexive
transitive
antisymmetric
with_suprema
with_infima
->
reflexive
transitive
antisymmetric
with_suprema
with_infima
complete
for ( ( ) ( )
RelStr
) ;
end;