:: WAYBEL23 semantic presentation
begin
theorem
:: WAYBEL23:1
for
L
being ( ( non
empty
reflexive
transitive
antisymmetric
) ( non
empty
reflexive
transitive
antisymmetric
)
Poset
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
compactbelow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
) ( non
empty
reflexive
transitive
antisymmetric
)
Poset
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
(
waybelow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
lower
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
) ( non
empty
reflexive
transitive
antisymmetric
)
Poset
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
/\
the
carrier
of
(
CompactSublatt
L
: ( ( non
empty
reflexive
transitive
antisymmetric
) ( non
empty
reflexive
transitive
antisymmetric
)
Poset
)
)
: ( (
strict
full
) (
strict
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
) ( non
empty
reflexive
transitive
antisymmetric
)
Poset
) ) : ( ( ) ( )
set
) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
) ( non
empty
reflexive
transitive
antisymmetric
)
Poset
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
definition
let
L
be ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ;
let
X
be ( ( ) ( )
Subset
of ) ;
:: original:
union
redefine
func
union
X
->
( ( ) ( )
Subset
of ) ;
end;
theorem
:: WAYBEL23:2
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
X
,
Y
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
c=
Y
: ( ( ) ( )
Subset
of ) holds
finsups
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
finsups
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:3
for
L
being ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
)
for
S
being ( ( non
empty
full
sups-inheriting
) ( non
empty
transitive
full
join-inheriting
sups-inheriting
directed-sups-inheriting
)
SubRelStr
of
L
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) )
for
X
being ( ( ) ( )
Subset
of )
for
Y
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
=
Y
: ( ( ) ( )
Subset
of ) holds
finsups
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
finsups
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
2
: ( ( non
empty
full
sups-inheriting
) ( non
empty
transitive
full
join-inheriting
sups-inheriting
directed-sups-inheriting
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:4
for
L
being ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
)
for
S
being ( ( non
empty
full
sups-inheriting
) ( non
empty
transitive
antisymmetric
full
join-inheriting
sups-inheriting
with_suprema
directed-sups-inheriting
)
SubRelStr
of
L
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) )
for
X
being ( ( ) ( )
Subset
of )
for
Y
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
=
Y
: ( ( ) ( )
Subset
of ) holds
finsups
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( non
empty
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
finsups
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
2
: ( ( non
empty
full
sups-inheriting
) ( non
empty
transitive
antisymmetric
full
join-inheriting
sups-inheriting
with_suprema
directed-sups-inheriting
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:5
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
complete
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
sup-Semilattice
)
for
S
being ( ( non
empty
full
join-inheriting
) ( non
empty
reflexive
transitive
antisymmetric
full
join-inheriting
with_suprema
)
SubRelStr
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
complete
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
sup-Semilattice
) ) st
Bottom
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
complete
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
sup-Semilattice
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
complete
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
in
the
carrier
of
S
: ( ( non
empty
full
join-inheriting
) ( non
empty
reflexive
transitive
antisymmetric
full
join-inheriting
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
complete
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
sup-Semilattice
) ) : ( ( ) ( non
empty
)
set
) holds
for
X
being ( ( ) ( )
Subset
of )
for
Y
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
=
Y
: ( ( ) ( )
Subset
of ) holds
finsups
Y
: ( ( ) ( )
Subset
of ) : ( ( ) (
directed
)
Element
of
K32
( the
carrier
of
b
2
: ( ( non
empty
full
join-inheriting
) ( non
empty
reflexive
transitive
antisymmetric
full
join-inheriting
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
complete
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
sup-Semilattice
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
finsups
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( non
empty
directed
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
complete
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:6
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
)
for
X
being ( ( ) ( )
Subset
of ) holds
sup
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of the
carrier
of
(
InclPoset
(
Ids
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
=
downarrow
(
finsups
(
union
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( non
empty
directed
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
directed
lower
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:7
for
L
being ( (
reflexive
transitive
) (
reflexive
transitive
)
RelStr
)
for
X
being ( ( ) ( )
Subset
of ) holds
downarrow
(
downarrow
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
) (
reflexive
transitive
)
RelStr
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
) (
reflexive
transitive
)
RelStr
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
=
downarrow
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
) (
reflexive
transitive
)
RelStr
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:8
for
L
being ( (
reflexive
transitive
) (
reflexive
transitive
)
RelStr
)
for
X
being ( ( ) ( )
Subset
of ) holds
uparrow
(
uparrow
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
) (
reflexive
transitive
)
RelStr
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
) (
reflexive
transitive
)
RelStr
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
=
uparrow
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
) (
reflexive
transitive
)
RelStr
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:9
for
L
being ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
downarrow
(
downarrow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
directed
lower
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
directed
lower
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
downarrow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
directed
lower
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:10
for
L
being ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
uparrow
(
uparrow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
filtered
upper
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
filtered
upper
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
uparrow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
filtered
upper
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:11
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
S
being ( ( non
empty
) ( non
empty
)
SubRelStr
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) )
for
X
being ( ( ) ( )
Subset
of )
for
Y
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
=
Y
: ( ( ) ( )
Subset
of ) holds
downarrow
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
SubRelStr
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
downarrow
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:12
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
S
being ( ( non
empty
) ( non
empty
)
SubRelStr
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) )
for
X
being ( ( ) ( )
Subset
of )
for
Y
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
=
Y
: ( ( ) ( )
Subset
of ) holds
uparrow
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
SubRelStr
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
uparrow
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:13
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
S
being ( ( non
empty
) ( non
empty
)
SubRelStr
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
downarrow
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
SubRelStr
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
downarrow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:14
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
S
being ( ( non
empty
) ( non
empty
)
SubRelStr
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
uparrow
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
SubRelStr
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
uparrow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
begin
definition
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
let
S
be ( ( ) ( )
Subset
of ) ;
attr
S
is
meet-closed
means
:: WAYBEL23:def 1
subrelstr
S
: ( ( ) ( )
NetStr
over
L
: ( ( ) ( )
1-sorted
) ) : ( (
strict
full
) (
strict
full
)
SubRelStr
of
L
: ( ( ) ( )
1-sorted
) ) is
meet-inheriting
;
end;
definition
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
let
S
be ( ( ) ( )
Subset
of ) ;
attr
S
is
join-closed
means
:: WAYBEL23:def 2
subrelstr
S
: ( ( ) ( )
NetStr
over
L
: ( ( ) ( )
1-sorted
) ) : ( (
strict
full
) (
strict
full
)
SubRelStr
of
L
: ( ( ) ( )
1-sorted
) ) is
join-inheriting
;
end;
definition
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
let
S
be ( ( ) ( )
Subset
of ) ;
attr
S
is
infs-closed
means
:: WAYBEL23:def 3
subrelstr
S
: ( ( ) ( )
NetStr
over
L
: ( ( ) ( )
1-sorted
) ) : ( (
strict
full
) (
strict
full
)
SubRelStr
of
L
: ( ( ) ( )
1-sorted
) ) is
infs-inheriting
;
end;
definition
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
let
S
be ( ( ) ( )
Subset
of ) ;
attr
S
is
sups-closed
means
:: WAYBEL23:def 4
subrelstr
S
: ( ( ) ( )
NetStr
over
L
: ( ( ) ( )
1-sorted
) ) : ( (
strict
full
) (
strict
full
)
SubRelStr
of
L
: ( ( ) ( )
1-sorted
) ) is
sups-inheriting
;
end;
registration
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
cluster
infs-closed
->
meet-closed
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
sups-closed
->
join-closed
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
cluster
non
empty
infs-closed
sups-closed
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: WAYBEL23:15
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
S
being ( ( ) ( )
Subset
of ) holds
(
S
: ( ( ) ( )
Subset
of ) is
meet-closed
iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) &
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) &
ex_inf_of
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ,
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
) ( non
empty
)
RelStr
) holds
inf
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ,
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: WAYBEL23:16
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
S
being ( ( ) ( )
Subset
of ) holds
(
S
: ( ( ) ( )
Subset
of ) is
join-closed
iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) &
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) &
ex_sup_of
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ,
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
) ( non
empty
)
RelStr
) holds
sup
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ,
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: WAYBEL23:17
for
L
being ( (
antisymmetric
with_infima
) ( non
empty
antisymmetric
with_infima
)
RelStr
)
for
S
being ( ( ) ( )
Subset
of ) holds
(
S
: ( ( ) ( )
Subset
of ) is
meet-closed
iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) &
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) holds
inf
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ,
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K32
( the
carrier
of
b
1
: ( (
antisymmetric
with_infima
) ( non
empty
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
antisymmetric
with_infima
) ( non
empty
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: WAYBEL23:18
for
L
being ( (
antisymmetric
with_suprema
) ( non
empty
antisymmetric
with_suprema
)
RelStr
)
for
S
being ( ( ) ( )
Subset
of ) holds
(
S
: ( ( ) ( )
Subset
of ) is
join-closed
iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) &
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) holds
sup
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ,
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K32
( the
carrier
of
b
1
: ( (
antisymmetric
with_suprema
) ( non
empty
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
antisymmetric
with_suprema
) ( non
empty
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: WAYBEL23:19
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
S
being ( ( ) ( )
Subset
of ) holds
(
S
: ( ( ) ( )
Subset
of ) is
infs-closed
iff for
X
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) st
ex_inf_of
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
) ( non
empty
)
RelStr
) holds
"/\"
(
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
) ( non
empty
)
RelStr
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: WAYBEL23:20
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
S
being ( ( ) ( )
Subset
of ) holds
(
S
: ( ( ) ( )
Subset
of ) is
sups-closed
iff for
X
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) st
ex_sup_of
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
) ( non
empty
)
RelStr
) holds
"\/"
(
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
) ( non
empty
)
RelStr
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: WAYBEL23:21
for
L
being ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
)
for
S
being ( ( non
empty
infs-closed
) ( non
empty
meet-closed
infs-closed
)
Subset
of )
for
X
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) st
ex_inf_of
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) holds
(
ex_inf_of
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
subrelstr
S
: ( ( non
empty
infs-closed
) ( non
empty
meet-closed
infs-closed
)
Subset
of ) : ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) &
"/\"
(
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
(
subrelstr
S
: ( ( non
empty
infs-closed
) ( non
empty
meet-closed
infs-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) ) : ( ( ) ( )
Element
of the
carrier
of
(
subrelstr
b
2
: ( ( non
empty
infs-closed
) ( non
empty
meet-closed
infs-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) )
=
"/\"
(
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: WAYBEL23:22
for
L
being ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
)
for
S
being ( ( non
empty
sups-closed
) ( non
empty
join-closed
sups-closed
)
Subset
of )
for
X
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) st
ex_sup_of
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) holds
(
ex_sup_of
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
subrelstr
S
: ( ( non
empty
sups-closed
) ( non
empty
join-closed
sups-closed
)
Subset
of ) : ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) &
"\/"
(
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
(
subrelstr
S
: ( ( non
empty
sups-closed
) ( non
empty
join-closed
sups-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) ) : ( ( ) ( )
Element
of the
carrier
of
(
subrelstr
b
2
: ( ( non
empty
sups-closed
) ( non
empty
join-closed
sups-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) )
=
"\/"
(
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: WAYBEL23:23
for
L
being ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
)
for
S
being ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of )
for
x
,
y
being ( ( ) ( )
Element
of
S
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) ) st
ex_inf_of
{
x
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) ) ,
y
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) )
}
: ( ( ) (
finite
)
Element
of
K32
(
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) ) : ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) holds
(
ex_inf_of
{
x
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) ) ,
y
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) )
}
: ( ( ) (
finite
)
Element
of
K32
(
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) ) : ( ( ) ( non
empty
)
set
) ) ,
subrelstr
S
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) : ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) &
"/\"
(
{
x
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) ) ,
y
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) )
}
: ( ( ) (
finite
)
Element
of
K32
(
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) ) : ( ( ) ( non
empty
)
set
) ) ,
(
subrelstr
S
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) ) : ( ( ) ( )
Element
of the
carrier
of
(
subrelstr
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) )
=
"/\"
(
{
x
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) ) ,
y
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) )
}
: ( ( ) (
finite
)
Element
of
K32
(
b
2
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) ) : ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: WAYBEL23:24
for
L
being ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
)
for
S
being ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of )
for
x
,
y
being ( ( ) ( )
Element
of
S
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) ) st
ex_sup_of
{
x
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) ) ,
y
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) )
}
: ( ( ) (
finite
)
Element
of
K32
(
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) ) : ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) holds
(
ex_sup_of
{
x
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) ) ,
y
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) )
}
: ( ( ) (
finite
)
Element
of
K32
(
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) ) : ( ( ) ( non
empty
)
set
) ) ,
subrelstr
S
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) : ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) &
"\/"
(
{
x
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) ) ,
y
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) )
}
: ( ( ) (
finite
)
Element
of
K32
(
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) ) : ( ( ) ( non
empty
)
set
) ) ,
(
subrelstr
S
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) ) : ( ( ) ( )
Element
of the
carrier
of
(
subrelstr
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) )
=
"\/"
(
{
x
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) ) ,
y
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) )
}
: ( ( ) (
finite
)
Element
of
K32
(
b
2
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) ) : ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
transitive
) ( non
empty
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: WAYBEL23:25
for
L
being ( (
transitive
antisymmetric
with_infima
) ( non
empty
transitive
antisymmetric
with_infima
)
RelStr
)
for
S
being ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) holds
subrelstr
S
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) : ( (
strict
full
) ( non
empty
strict
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( (
transitive
antisymmetric
with_infima
) ( non
empty
transitive
antisymmetric
with_infima
)
RelStr
) ) is
with_infima
;
theorem
:: WAYBEL23:26
for
L
being ( (
transitive
antisymmetric
with_suprema
) ( non
empty
transitive
antisymmetric
with_suprema
)
RelStr
)
for
S
being ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) holds
subrelstr
S
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) : ( (
strict
full
) ( non
empty
strict
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( (
transitive
antisymmetric
with_suprema
) ( non
empty
transitive
antisymmetric
with_suprema
)
RelStr
) ) is
with_suprema
;
registration
let
L
be ( (
transitive
antisymmetric
with_infima
) ( non
empty
transitive
antisymmetric
with_infima
)
RelStr
) ;
let
S
be ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Subset
of ) ;
cluster
subrelstr
S
: ( ( non
empty
meet-closed
) ( non
empty
meet-closed
)
Element
of
K32
( the
carrier
of
L
: ( (
transitive
antisymmetric
with_infima
) ( non
empty
transitive
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
full
) ( non
empty
strict
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( (
transitive
antisymmetric
with_infima
) ( non
empty
transitive
antisymmetric
with_infima
)
RelStr
) )
->
strict
full
with_infima
;
end;
registration
let
L
be ( (
transitive
antisymmetric
with_suprema
) ( non
empty
transitive
antisymmetric
with_suprema
)
RelStr
) ;
let
S
be ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Subset
of ) ;
cluster
subrelstr
S
: ( ( non
empty
join-closed
) ( non
empty
join-closed
)
Element
of
K32
( the
carrier
of
L
: ( (
transitive
antisymmetric
with_suprema
) ( non
empty
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
full
) ( non
empty
strict
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( (
transitive
antisymmetric
with_suprema
) ( non
empty
transitive
antisymmetric
with_suprema
)
RelStr
) )
->
strict
full
with_suprema
;
end;
theorem
:: WAYBEL23:27
for
L
being ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
)
for
S
being ( ( non
empty
infs-closed
) ( non
empty
meet-closed
infs-closed
)
Subset
of )
for
X
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
"/\"
(
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
(
subrelstr
S
: ( ( non
empty
infs-closed
) ( non
empty
meet-closed
infs-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
antisymmetric
full
with_infima
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) ) ) : ( ( ) ( )
Element
of the
carrier
of
(
subrelstr
b
2
: ( ( non
empty
infs-closed
) ( non
empty
meet-closed
infs-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
antisymmetric
full
with_infima
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) )
=
"/\"
(
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:28
for
L
being ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
)
for
S
being ( ( non
empty
sups-closed
) ( non
empty
join-closed
sups-closed
)
Subset
of )
for
X
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
"\/"
(
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
(
subrelstr
S
: ( ( non
empty
sups-closed
) ( non
empty
join-closed
sups-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
antisymmetric
full
with_suprema
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) ) ) : ( ( ) ( )
Element
of the
carrier
of
(
subrelstr
b
2
: ( ( non
empty
sups-closed
) ( non
empty
join-closed
sups-closed
)
Subset
of )
)
: ( (
strict
full
) ( non
empty
strict
transitive
antisymmetric
full
with_suprema
)
SubRelStr
of
b
1
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) )
=
"\/"
(
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
transitive
antisymmetric
complete
) ( non
empty
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:29
for
L
being ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
)
for
S
being ( (
meet-closed
) (
meet-closed
)
Subset
of ) holds
S
: ( (
meet-closed
) (
meet-closed
)
Subset
of ) is
filtered
;
theorem
:: WAYBEL23:30
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
)
for
S
being ( (
join-closed
) (
join-closed
)
Subset
of ) holds
S
: ( (
join-closed
) (
join-closed
)
Subset
of ) is
directed
;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
) ;
cluster
meet-closed
->
filtered
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
) ;
cluster
join-closed
->
directed
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: WAYBEL23:31
for
L
being ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
)
for
S
being ( ( non
empty
upper
) ( non
empty
upper
)
Subset
of ) holds
(
S
: ( ( non
empty
upper
) ( non
empty
upper
)
Subset
of ) is ( ( non
empty
filtered
upper
) ( non
empty
filtered
upper
)
Filter
of
L
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
) ) iff
S
: ( ( non
empty
upper
) ( non
empty
upper
)
Subset
of ) is
meet-closed
) ;
theorem
:: WAYBEL23:32
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
)
for
S
being ( ( non
empty
lower
) ( non
empty
lower
)
Subset
of ) holds
(
S
: ( ( non
empty
lower
) ( non
empty
lower
)
Subset
of ) is ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
) ) iff
S
: ( ( non
empty
lower
) ( non
empty
lower
)
Subset
of ) is
join-closed
) ;
theorem
:: WAYBEL23:33
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
S1
,
S2
being ( (
join-closed
) (
join-closed
)
Subset
of ) holds
S1
: ( (
join-closed
) (
join-closed
)
Subset
of )
/\
S2
: ( (
join-closed
) (
join-closed
)
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
join-closed
;
theorem
:: WAYBEL23:34
for
L
being ( ( non
empty
) ( non
empty
)
RelStr
)
for
S1
,
S2
being ( (
meet-closed
) (
meet-closed
)
Subset
of ) holds
S1
: ( (
meet-closed
) (
meet-closed
)
Subset
of )
/\
S2
: ( (
meet-closed
) (
meet-closed
)
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
meet-closed
;
theorem
:: WAYBEL23:35
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
downarrow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
directed
lower
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
join-closed
;
theorem
:: WAYBEL23:36
for
L
being ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
downarrow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
directed
lower
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
meet-closed
;
theorem
:: WAYBEL23:37
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
uparrow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
filtered
upper
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
join-closed
;
theorem
:: WAYBEL23:38
for
L
being ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
uparrow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
filtered
upper
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
meet-closed
;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
) ;
let
x
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
downarrow
x
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
directed
lower
)
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
->
join-closed
;
cluster
uparrow
x
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
filtered
upper
)
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
->
join-closed
;
end;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
) ;
let
x
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
downarrow
x
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
directed
lower
)
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
->
meet-closed
;
cluster
uparrow
x
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
filtered
upper
)
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
->
meet-closed
;
end;
theorem
:: WAYBEL23:39
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
waybelow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
directed
lower
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
join-closed
;
theorem
:: WAYBEL23:40
for
L
being ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
waybelow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
lower
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
meet-closed
;
theorem
:: WAYBEL23:41
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
wayabove
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
upper
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
join-closed
;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
) ;
let
x
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
waybelow
x
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
directed
lower
)
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
->
join-closed
;
cluster
wayabove
x
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
upper
)
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
->
join-closed
;
end;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
Semilattice
) ;
let
x
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
waybelow
x
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
lower
)
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
with_infima
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
->
meet-closed
;
end;
begin
definition
let
T
be ( ( ) ( )
TopStruct
) ;
func
weight
T
->
( (
cardinal
) (
ordinal
cardinal
)
Cardinal
)
equals
:: WAYBEL23:def 5
meet
{
(
card
B
: ( (
V63
(
T
: ( ( ) ( )
TopStruct
) )
V231
(
T
: ( ( ) ( )
TopStruct
) ) ) (
V63
(
T
: ( ( ) ( )
TopStruct
) )
V231
(
T
: ( ( ) ( )
TopStruct
) ) )
Basis
of
T
: ( ( ) ( )
TopStruct
) )
)
: ( (
cardinal
) (
ordinal
cardinal
)
set
) where
B
is ( (
V63
(
T
: ( ( non
empty
) ( non
empty
)
RelStr
) )
V231
(
T
: ( ( non
empty
) ( non
empty
)
RelStr
) ) ) (
V63
(
T
: ( ( non
empty
) ( non
empty
)
RelStr
) )
V231
(
T
: ( ( non
empty
) ( non
empty
)
RelStr
) ) )
Basis
of
T
: ( ( non
empty
) ( non
empty
)
RelStr
) ) : verum
}
: ( ( ) ( )
set
) ;
end;
definition
let
T
be ( ( ) ( )
TopStruct
) ;
attr
T
is
second-countable
means
:: WAYBEL23:def 6
weight
T
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( (
cardinal
) (
ordinal
cardinal
)
Cardinal
)
c=
omega
: ( ( ) ( non
trivial
ordinal
non
finite
cardinal
limit_cardinal
)
set
) ;
end;
definition
let
L
be ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ;
mode
CLbasis
of
L
->
( ( ) ( )
Subset
of )
means
:: WAYBEL23:def 7
(
it
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
join-closed
& ( for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
sup
(
(
waybelow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
/\
it
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ) );
end;
definition
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
let
S
be ( ( ) ( )
Subset
of ) ;
attr
S
is
with_bottom
means
:: WAYBEL23:def 8
Bottom
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( )
Element
of the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
in
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
let
S
be ( ( ) ( )
Subset
of ) ;
attr
S
is
with_top
means
:: WAYBEL23:def 9
Top
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( )
Element
of the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
in
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
cluster
with_bottom
->
non
empty
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
cluster
with_top
->
non
empty
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
L
be ( ( non
empty
) ( non
empty
)
RelStr
) ;
cluster
with_bottom
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
with_top
for ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( ( non
empty
) ( non
empty
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ;
cluster
with_bottom
for ( ( ) ( )
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) ) ;
cluster
with_top
for ( ( ) ( )
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) ) ;
end;
theorem
:: WAYBEL23:42
for
L
being ( ( non
empty
antisymmetric
lower-bounded
) ( non
empty
antisymmetric
lower-bounded
)
RelStr
)
for
S
being ( (
with_bottom
) ( non
empty
with_bottom
)
Subset
of ) holds
subrelstr
S
: ( (
with_bottom
) ( non
empty
with_bottom
)
Subset
of ) : ( (
strict
full
) ( non
empty
strict
antisymmetric
full
)
SubRelStr
of
b
1
: ( ( non
empty
antisymmetric
lower-bounded
) ( non
empty
antisymmetric
lower-bounded
)
RelStr
) ) is
lower-bounded
;
registration
let
L
be ( ( non
empty
antisymmetric
lower-bounded
) ( non
empty
antisymmetric
lower-bounded
)
RelStr
) ;
let
S
be ( (
with_bottom
) ( non
empty
with_bottom
)
Subset
of ) ;
cluster
subrelstr
S
: ( (
with_bottom
) ( non
empty
with_bottom
)
Element
of
K32
( the
carrier
of
L
: ( ( non
empty
antisymmetric
lower-bounded
) ( non
empty
antisymmetric
lower-bounded
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
full
) ( non
empty
strict
antisymmetric
full
)
SubRelStr
of
L
: ( ( non
empty
antisymmetric
lower-bounded
) ( non
empty
antisymmetric
lower-bounded
)
RelStr
) )
->
strict
lower-bounded
full
;
end;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ;
cluster
->
join-closed
for ( ( ) ( )
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) ) ;
end;
registration
cluster
non
empty
non
trivial
reflexive
transitive
antisymmetric
upper-bounded
bounded
with_suprema
with_infima
up-complete
satisfying_axiom_of_approximation
continuous
for ( ( ) ( )
RelStr
) ;
end;
registration
let
L
be ( ( non
trivial
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
non
trivial
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ;
cluster
->
non
empty
for ( ( ) ( )
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) ) ;
end;
theorem
:: WAYBEL23:43
for
L
being ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
) holds the
carrier
of
(
CompactSublatt
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
)
)
: ( (
strict
full
) (
strict
reflexive
transitive
antisymmetric
full
join-inheriting
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
with_suprema
)
sup-Semilattice
) ) : ( ( ) ( )
set
) is ( (
join-closed
) (
directed
join-closed
)
Subset
of ) ;
theorem
:: WAYBEL23:44
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
algebraic
with_suprema
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
satisfying_axiom_K
algebraic
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) holds the
carrier
of
(
CompactSublatt
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
algebraic
with_suprema
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
satisfying_axiom_K
algebraic
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
)
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
full
join-inheriting
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
algebraic
with_suprema
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
satisfying_axiom_K
algebraic
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) : ( ( ) ( )
set
) is ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
algebraic
with_suprema
with_infima
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
satisfying_axiom_K
algebraic
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) ;
theorem
:: WAYBEL23:45
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) st the
carrier
of
(
CompactSublatt
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
full
join-inheriting
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( ( ) ( )
set
) is ( ( ) (
directed
join-closed
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) is
algebraic
;
theorem
:: WAYBEL23:46
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
)
for
B
being ( (
join-closed
) (
directed
join-closed
)
Subset
of ) holds
(
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) is ( ( ) (
directed
join-closed
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st not
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
ex
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) & not
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<<
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: WAYBEL23:47
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
)
for
B
being ( (
join-closed
) (
directed
join-closed
)
Subset
of ) st
Bottom
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
in
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) holds
(
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) is ( ( ) (
directed
join-closed
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<<
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
ex
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<<
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: WAYBEL23:48
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
)
for
B
being ( (
join-closed
) (
directed
join-closed
)
Subset
of ) st
Bottom
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
in
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) holds
(
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) is ( ( ) (
directed
join-closed
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) iff ( the
carrier
of
(
CompactSublatt
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
)
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
full
join-inheriting
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) : ( ( ) ( )
set
)
c=
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) & ( for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st not
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
ex
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) & not
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ) ) ;
theorem
:: WAYBEL23:49
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
)
for
B
being ( (
join-closed
) (
directed
join-closed
)
Subset
of ) st
Bottom
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
in
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) holds
(
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) is ( ( ) (
directed
join-closed
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st not
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
ex
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
B
: ( (
join-closed
) (
directed
join-closed
)
Subset
of ) & not
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: WAYBEL23:50
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
)
for
S
being ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) ) st
Bottom
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
in
the
carrier
of
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) ) : ( ( ) ( non
empty
)
set
) & the
carrier
of
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) ) : ( ( ) ( non
empty
)
set
) is ( (
join-closed
) (
directed
join-closed
)
Subset
of ) holds
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
waybelow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
directed
lower
join-closed
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
/\
the
carrier
of
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) ) : ( ( ) ( non
empty
)
set
) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
)
sup-Semilattice
) ) ) ;
definition
let
L
be ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ;
let
S
be ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) ;
func
supMap
S
->
( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
)
)
: ( (
strict
) (
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( )
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( non
empty
)
set
) )
means
:: WAYBEL23:def 10
for
I
being ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
it
: ( ( ) (
V7
()
V10
(
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V11
(
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) )
Element
of
K32
(
K33
(
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ,
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
.
I
: ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) ) : ( ( ) ( )
set
)
=
"\/"
(
I
: ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) ) ,
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) ) : ( ( ) ( )
Element
of the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
L
be ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ;
let
S
be ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) ;
func
idsMap
S
->
( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
)
)
: ( (
strict
) (
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( )
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
with_suprema
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( non
empty
)
set
) )
means
:: WAYBEL23:def 11
for
I
being ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ex
J
being ( ( ) ( )
Subset
of ) st
(
I
: ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) )
=
J
: ( ( ) ( )
Subset
of ) &
it
: ( ( ) (
V7
()
V10
(
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V11
(
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) )
Element
of
K32
(
K33
(
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ,
S
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
.
I
: ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) ) : ( ( ) ( )
set
)
=
downarrow
J
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) );
end;
registration
let
L
be ( (
reflexive
) (
reflexive
)
RelStr
) ;
let
B
be ( ( ) ( )
Subset
of ) ;
cluster
subrelstr
B
: ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
) (
reflexive
)
RelStr
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
full
) (
strict
reflexive
full
)
SubRelStr
of
L
: ( (
reflexive
) (
reflexive
)
RelStr
) )
->
strict
reflexive
full
;
end;
registration
let
L
be ( (
transitive
) (
transitive
)
RelStr
) ;
let
B
be ( ( ) ( )
Subset
of ) ;
cluster
subrelstr
B
: ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( (
transitive
) (
transitive
)
RelStr
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
full
) (
strict
transitive
full
)
SubRelStr
of
L
: ( (
transitive
) (
transitive
)
RelStr
) )
->
strict
transitive
full
;
end;
registration
let
L
be ( (
antisymmetric
) (
antisymmetric
)
RelStr
) ;
let
B
be ( ( ) ( )
Subset
of ) ;
cluster
subrelstr
B
: ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( (
antisymmetric
) (
antisymmetric
)
RelStr
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
full
) (
strict
antisymmetric
full
)
SubRelStr
of
L
: ( (
antisymmetric
) (
antisymmetric
)
RelStr
) )
->
strict
antisymmetric
full
;
end;
definition
let
L
be ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ;
let
B
be ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) ;
func
baseMap
B
->
( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
B
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
full
) (
strict
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) )
)
: ( ( ) ( )
set
)
)
: ( (
strict
) (
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( )
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( )
set
) )
means
:: WAYBEL23:def 12
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
it
: ( ( ) (
V7
()
V10
(
B
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V11
(
B
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) )
Element
of
K32
(
K33
(
B
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ,
B
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
.
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
B
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
full
) (
strict
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) )
)
: ( ( ) ( )
set
)
)
: ( (
strict
) (
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( )
set
) )
=
(
waybelow
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
/\
B
: ( (
Function-like
quasi_total
closure
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
closure
)
Element
of
K32
(
K33
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
upper-bounded
with_suprema
up-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: WAYBEL23:51
for
L
being ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
for
S
being ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) holds
(
dom
(
supMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
Ids
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) &
rng
(
supMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
Subset
of ) ) ;
theorem
:: WAYBEL23:52
for
L
being ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
for
S
being ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
dom
(
supMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) iff
x
: ( ( ) ( )
set
) is ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) ) ) ;
theorem
:: WAYBEL23:53
for
L
being ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
for
S
being ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) holds
(
dom
(
idsMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
Ids
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) : ( ( ) ( non
empty
)
set
) &
rng
(
idsMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: WAYBEL23:54
for
L
being ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
for
S
being ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
dom
(
idsMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) iff
x
: ( ( ) ( )
set
) is ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) ) ) ;
theorem
:: WAYBEL23:55
for
L
being ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
for
S
being ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
rng
(
idsMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
set
) is ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) ;
theorem
:: WAYBEL23:56
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds
(
dom
(
baseMap
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) &
rng
(
baseMap
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: WAYBEL23:57
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
rng
(
baseMap
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
set
) is ( ( non
empty
directed
lower
) ( non
empty
directed
lower
)
Ideal
of
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) ) ;
theorem
:: WAYBEL23:58
for
L
being ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
)
for
S
being ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) ) holds
supMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
monotone
;
theorem
:: WAYBEL23:59
for
L
being ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
for
S
being ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) holds
idsMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
monotone
;
theorem
:: WAYBEL23:60
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds
baseMap
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
monotone
;
registration
let
L
be ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) ;
let
S
be ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) ) ;
cluster
supMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
RelStr
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
->
Function-like
quasi_total
monotone
;
end;
registration
let
L
be ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ;
let
S
be ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) ;
cluster
idsMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
L
: ( ( non
empty
reflexive
transitive
) ( non
empty
reflexive
transitive
)
RelStr
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
->
Function-like
quasi_total
monotone
;
end;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ;
let
B
be ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) ;
cluster
baseMap
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
->
Function-like
quasi_total
monotone
;
end;
theorem
:: WAYBEL23:61
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds
idsMap
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
sups-preserving
;
theorem
:: WAYBEL23:62
for
L
being ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
)
for
S
being ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
L
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) ) holds
supMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
=
(
SupMap
L
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
)
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Element
of
K32
(
K33
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
*
(
idsMap
S
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
)
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( (
Function-like
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) : ( ( ) ( non
empty
)
set
) )
Function-like
)
Element
of
K32
(
K33
( the
carrier
of
(
InclPoset
(
Ids
b
2
: ( ( non
empty
full
) ( non
empty
reflexive
transitive
antisymmetric
full
)
SubRelStr
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
)
RelStr
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
reflexive
transitive
antisymmetric
up-complete
) ( non
empty
reflexive
transitive
antisymmetric
up-complete
)
Poset
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:63
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds
[
(
supMap
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) ,
(
baseMap
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
]
: ( ( ) ( )
Connection
of
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
) : ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) ,
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) is
Galois
;
theorem
:: WAYBEL23:64
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds
(
supMap
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
upper_adjoint
&
baseMap
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
lower_adjoint
) ;
theorem
:: WAYBEL23:65
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds
rng
(
supMap
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) ;
theorem
:: WAYBEL23:66
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds
(
supMap
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
infs-preserving
&
supMap
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
sups-preserving
) ;
theorem
:: WAYBEL23:67
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds
baseMap
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
sups-preserving
;
registration
let
L
be ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ;
let
B
be ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) ;
cluster
supMap
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
->
Function-like
quasi_total
infs-preserving
sups-preserving
;
cluster
baseMap
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) ) : ( (
Function-like
quasi_total
) (
V7
()
V10
( the
carrier
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
V11
( the
carrier
of
(
InclPoset
(
Ids
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
RelStr
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( ( ) ( non
empty
)
set
) )
Function-like
quasi_total
monotone
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
->
Function-like
quasi_total
sups-preserving
;
end;
theorem
:: WAYBEL23:68
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds the
carrier
of
(
CompactSublatt
(
InclPoset
(
Ids
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
)
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
full
join-inheriting
with_suprema
)
SubRelStr
of
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
) : ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) ) : ( ( ) ( non
empty
)
set
)
=
{
(
downarrow
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
directed
lower
join-closed
)
Element
of
K32
( the
carrier
of
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) where
b
is ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : verum
}
;
theorem
:: WAYBEL23:69
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) holds
CompactSublatt
(
InclPoset
(
Ids
(
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
)
)
: ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) : ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
full
join-inheriting
with_suprema
)
SubRelStr
of
InclPoset
(
Ids
(
subrelstr
b
2
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
)
: ( ( ) ( non
empty
)
set
) : ( (
strict
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
)
RelStr
) ) ,
subrelstr
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) ) : ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
lower-bounded
full
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
sup-Semilattice
) )
are_isomorphic
;
theorem
:: WAYBEL23:70
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
)
for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) st ( for
B1
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) holds
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) )
c=
B1
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) holds
for
J
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
J
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
waybelow
(
"\/"
(
J
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ,
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
directed
filtered
lower
meet-closed
join-closed
)
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
/\
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: WAYBEL23:71
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) holds
(
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) is
algebraic
iff ( the
carrier
of
(
CompactSublatt
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
)
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
full
join-inheriting
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) : ( ( ) ( non
empty
)
set
) is ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) & ( for
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) holds the
carrier
of
(
CompactSublatt
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
)
)
: ( (
strict
full
) ( non
empty
strict
reflexive
transitive
antisymmetric
full
join-inheriting
with_suprema
)
SubRelStr
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) : ( ( ) ( non
empty
)
set
)
c=
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) ) ) ) ;
theorem
:: WAYBEL23:72
for
L
being ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) holds
(
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) is
algebraic
iff ex
B
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) st
for
B1
being ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
L
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) holds
B
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) )
c=
B1
: ( (
with_bottom
) ( non
empty
directed
join-closed
with_bottom
)
CLbasis
of
b
1
: ( (
reflexive
transitive
antisymmetric
lower-bounded
with_suprema
with_infima
continuous
) ( non
empty
reflexive
transitive
antisymmetric
lower-bounded
upper-bounded
bounded
with_suprema
with_infima
complete
up-complete
/\-complete
satisfying_axiom_of_approximation
continuous
)
LATTICE
) ) ) ;
theorem
:: WAYBEL23:73
for
T
being ( ( ) ( )
TopStruct
)
for
b
being ( (
V63
(
b
1
: ( ( ) ( )
TopStruct
) )
V231
(
b
1
: ( ( ) ( )
TopStruct
) ) ) (
V63
(
b
1
: ( ( ) ( )
TopStruct
) )
V231
(
b
1
: ( ( ) ( )
TopStruct
) ) )
Basis
of
T
: ( ( ) ( )
TopStruct
) ) holds
weight
T
: ( ( ) ( )
TopStruct
) : ( (
cardinal
) (
ordinal
cardinal
)
Cardinal
)
c=
card
b
: ( (
V63
(
b
1
: ( ( ) ( )
TopStruct
) )
V231
(
b
1
: ( ( ) ( )
TopStruct
) ) ) (
V63
(
b
1
: ( ( ) ( )
TopStruct
) )
V231
(
b
1
: ( ( ) ( )
TopStruct
) ) )
Basis
of
b
1
: ( ( ) ( )
TopStruct
) ) : ( (
cardinal
) (
ordinal
cardinal
)
set
) ;
theorem
:: WAYBEL23:74
for
T
being ( ( ) ( )
TopStruct
) ex
b
being ( (
V63
(
b
1
: ( ( ) ( )
TopStruct
) )
V231
(
b
1
: ( ( ) ( )
TopStruct
) ) ) (
V63
(
b
1
: ( ( ) ( )
TopStruct
) )
V231
(
b
1
: ( ( ) ( )
TopStruct
) ) )
Basis
of
T
: ( ( ) ( )
TopStruct
) ) st
card
b
: ( (
V63
(
b
1
: ( ( ) ( )
TopStruct
) )
V231
(
b
1
: ( ( ) ( )
TopStruct
) ) ) (
V63
(
b
1
: ( ( ) ( )
TopStruct
) )
V231
(
b
1
: ( ( ) ( )
TopStruct
) ) )
Basis
of
b
1
: ( ( ) ( )
TopStruct
) ) : ( (
cardinal
) (
ordinal
cardinal
)
set
)
=
weight
T
: ( ( ) ( )
TopStruct
) : ( (
cardinal
) (
ordinal
cardinal
)
Cardinal
) ;