:: WAYBEL_6 semantic presentation

REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V42() V43() Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V42() V43() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K257() is L6()
the carrier of K257() is set
{} is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V36() finite finite-yielding V41() V42() V44( {} ) set
the empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V36() finite finite-yielding V41() V42() V44( {} ) set is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V36() finite finite-yielding V41() V42() V44( {} ) set
1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
{{},1} is non empty finite V41() set
[:1,1:] is non empty Relation-like finite set
bool [:1,1:] is non empty finite V41() set
[:[:1,1:],1:] is non empty Relation-like finite set
bool [:[:1,1:],1:] is non empty finite V41() set
0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V36() finite finite-yielding V41() V42() V44( {} ) Element of NAT
{{}} is non empty trivial functional finite V41() V44(1) set
F₁() is non empty RelStr
the carrier of F₁() is non empty set
bool the carrier of F₁() is non empty set
F₂() is Element of bool the carrier of F₁()
F₃() is non empty Element of bool the carrier of F₁()
[:F₂(),F₃():] is Relation-like set
bool [:F₂(),F₃():] is non empty set
L is set
L is Element of F₂()
L is Element of the carrier of F₁()
l1 is Element of the carrier of F₁()
Y is set
L is Relation-like Function-like set
dom L is set
rng L is set
L is Relation-like F₂() -defined F₃() -valued Function-like V32(F₂(),F₃()) Element of bool [:F₂(),F₃():]
L is Element of the carrier of F₁()
L . L is set
l1 is Element of F₃()
Y is Element of the carrier of F₁()
L is Element of the carrier of F₁()
L . L is set
L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is non empty Element of bool the carrier of L
[:L,L:] is non empty Relation-like set
bool [:L,L:] is non empty set
L is Relation-like L -defined L -valued Function-like V32(L,L) Element of bool [:L,L:]
l1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
iter (L,l1) is Relation-like set
L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is non empty Element of bool the carrier of L
L is non empty Element of bool the carrier of L
[:L,L:] is non empty Relation-like set
bool [:L,L:] is non empty set
l1 is Relation-like L -defined L -valued Function-like V32(L,L) Element of bool [:L,L:]
Y is Element of L
l1 . Y is set
l1 . Y is Element of L
L is non empty V110() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is strongly_connected Element of bool the carrier of L
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V28( the carrier of L) reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is Element of the carrier of L
l1 is Element of the carrier of L
[L,l1] is Element of [: the carrier of L, the carrier of L:]
{L,l1} is non empty finite set
{L} is non empty trivial finite V44(1) set
{{L,l1},{L}} is non empty finite V41() set
[l1,L] is Element of [: the carrier of L, the carrier of L:]
{l1,L} is non empty finite set
{l1} is non empty trivial finite V44(1) set
{{l1,L},{l1}} is non empty finite V41() set
L is Element of the carrier of L
l1 is Element of the carrier of L
[L,l1] is Element of [: the carrier of L, the carrier of L:]
{L,l1} is non empty finite set
{L} is non empty trivial finite V44(1) set
{{L,l1},{L}} is non empty finite V41() set
[l1,L] is Element of [: the carrier of L, the carrier of L:]
{l1,L} is non empty finite set
{l1} is non empty trivial finite V44(1) set
{{l1,L},{l1}} is non empty finite V41() set
the set is set
{ the set } is non empty trivial finite V44(1) set
[:{ the set },{ the set }:] is non empty Relation-like finite set
bool [:{ the set },{ the set }:] is non empty finite V41() set
the Relation-like { the set } -defined { the set } -valued V28({ the set }) finite reflexive antisymmetric transitive Element of bool [:{ the set },{ the set }:] is Relation-like { the set } -defined { the set } -valued V28({ the set }) finite reflexive antisymmetric transitive Element of bool [:{ the set },{ the set }:]
RelStr(# { the set }, the Relation-like { the set } -defined { the set } -valued V28({ the set }) finite reflexive antisymmetric transitive Element of bool [:{ the set },{ the set }:] #) is non empty trivial finite 1 -element strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() connected up-complete /\-complete distributive Heyting complemented Boolean with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous completely-distributive RelStr
L is non empty trivial finite 1 -element V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() connected up-complete /\-complete distributive Heyting complemented Boolean with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous completely-distributive RelStr
L is non empty V110() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
L is non empty V110() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
dom L is Element of bool the carrier of L
bool the carrier of L is non empty set
l1 is Element of the carrier of L
Y is Element of the carrier of L
l1 "/\" Y is Element of the carrier of L
L . (l1 "/\" Y) is Element of the carrier of L
L . l1 is Element of the carrier of L
L . Y is Element of the carrier of L
(L . l1) "/\" (L . Y) is Element of the carrier of L
{l1,Y} is non empty finite Element of bool the carrier of L
L .: {l1,Y} is non empty finite Element of bool the carrier of L
bool the carrier of L is non empty set
{(L . l1),(L . Y)} is non empty finite Element of bool the carrier of L
"/\" ({l1,Y},L) is Element of the carrier of L
L . ("/\" ({l1,Y},L)) is Element of the carrier of L
"/\" ({(L . l1),(L . Y)},L) is Element of the carrier of L
l1 is Element of the carrier of L
Y is Element of the carrier of L
{l1,Y} is non empty finite Element of bool the carrier of L
L .: {l1,Y} is non empty finite Element of bool the carrier of L
bool the carrier of L is non empty set
L . l1 is Element of the carrier of L
L . Y is Element of the carrier of L
{(L . l1),(L . Y)} is non empty finite Element of bool the carrier of L
"/\" ((L .: {l1,Y}),L) is Element of the carrier of L
(L . l1) "/\" (L . Y) is Element of the carrier of L
l1 "/\" Y is Element of the carrier of L
L . (l1 "/\" Y) is Element of the carrier of L
"/\" ({l1,Y},L) is Element of the carrier of L
L . ("/\" ({l1,Y},L)) is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
L is non empty V110() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
dom L is Element of bool the carrier of L
bool the carrier of L is non empty set
l1 is Element of the carrier of L
Y is Element of the carrier of L
l1 "\/" Y is Element of the carrier of L
L . (l1 "\/" Y) is Element of the carrier of L
L . l1 is Element of the carrier of L
L . Y is Element of the carrier of L
(L . l1) "\/" (L . Y) is Element of the carrier of L
{l1,Y} is non empty finite Element of bool the carrier of L
L .: {l1,Y} is non empty finite Element of bool the carrier of L
bool the carrier of L is non empty set
{(L . l1),(L . Y)} is non empty finite Element of bool the carrier of L
"\/" ({l1,Y},L) is Element of the carrier of L
L . ("\/" ({l1,Y},L)) is Element of the carrier of L
"\/" ({(L . l1),(L . Y)},L) is Element of the carrier of L
l1 is Element of the carrier of L
Y is Element of the carrier of L
{l1,Y} is non empty finite Element of bool the carrier of L
L .: {l1,Y} is non empty finite Element of bool the carrier of L
bool the carrier of L is non empty set
L . l1 is Element of the carrier of L
L . Y is Element of the carrier of L
{(L . l1),(L . Y)} is non empty finite Element of bool the carrier of L
"\/" ((L .: {l1,Y}),L) is Element of the carrier of L
(L . l1) "\/" (L . Y) is Element of the carrier of L
l1 "\/" Y is Element of the carrier of L
L . (l1 "\/" Y) is Element of the carrier of L
"\/" ({l1,Y},L) is Element of the carrier of L
L . ("\/" ({l1,Y},L)) is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
l1 is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
Y "\/" Y is Element of the carrier of L
l1 "/\" (Y "\/" Y) is Element of the carrier of L
l1 "/\" Y is Element of the carrier of L
l1 "/\" Y is Element of the carrier of L
(l1 "/\" Y) "\/" (l1 "/\" Y) is Element of the carrier of L
Y "\/" Y is Element of the carrier of L
l1 "/\" (Y "\/" Y) is Element of the carrier of L
L . (l1 "/\" (Y "\/" Y)) is Element of the carrier of L
L . l1 is Element of the carrier of L
L . (Y "\/" Y) is Element of the carrier of L
(L . l1) "/\" (L . (Y "\/" Y)) is Element of the carrier of L
L . Y is Element of the carrier of L
L . Y is Element of the carrier of L
(L . Y) "\/" (L . Y) is Element of the carrier of L
(L . l1) "/\" ((L . Y) "\/" (L . Y)) is Element of the carrier of L
(L . l1) "/\" (L . Y) is Element of the carrier of L
(L . l1) "/\" (L . Y) is Element of the carrier of L
((L . l1) "/\" (L . Y)) "\/" ((L . l1) "/\" (L . Y)) is Element of the carrier of L
l1 "/\" Y is Element of the carrier of L
L . (l1 "/\" Y) is Element of the carrier of L
((L . l1) "/\" (L . Y)) "\/" (L . (l1 "/\" Y)) is Element of the carrier of L
l1 "/\" Y is Element of the carrier of L
L . (l1 "/\" Y) is Element of the carrier of L
(L . (l1 "/\" Y)) "\/" (L . (l1 "/\" Y)) is Element of the carrier of L
(l1 "/\" Y) "\/" (l1 "/\" Y) is Element of the carrier of L
L . ((l1 "/\" Y) "\/" (l1 "/\" Y)) is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
Bottom L is Element of the carrier of L
L --> (Bottom L) is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
the carrier of L --> (Bottom L) is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like constant V28( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
bool the carrier of L is non empty set
Y is Element of bool the carrier of L
(L --> (Bottom L)) .: Y is Element of bool the carrier of L
bool the carrier of L is non empty set
"\/" (((L --> (Bottom L)) .: Y),L) is Element of the carrier of L
"\/" (Y,L) is Element of the carrier of L
(L --> (Bottom L)) . ("\/" (Y,L)) is Element of the carrier of L
rng (L --> (Bottom L)) is Element of bool the carrier of L
{(Bottom L)} is non empty trivial finite V44(1) Element of bool the carrier of L
Y is non empty Element of bool the carrier of L
the Element of Y is Element of Y
(L --> (Bottom L)) . the Element of Y is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
L is non empty V110() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
l1 is Element of the carrier of L
Y is Element of the carrier of L
L . l1 is set
L . Y is set
Y "\/" l1 is Element of the carrier of L
{l1,Y} is non empty finite Element of bool the carrier of L
bool the carrier of L is non empty set
Y is Element of the carrier of L
x is Element of the carrier of L
dom L is Element of bool the carrier of L
Y is Element of the carrier of L
L .: {l1,Y} is non empty finite Element of bool the carrier of L
bool the carrier of L is non empty set
"\/" ((L .: {l1,Y}),L) is Element of the carrier of L
"\/" ({l1,Y},L) is Element of the carrier of L
L . ("\/" ({l1,Y},L)) is Element of the carrier of L
L . Y is Element of the carrier of L
L . l1 is Element of the carrier of L
{(L . l1),(L . Y)} is non empty finite Element of bool the carrier of L
"\/" ({(L . l1),(L . Y)},L) is Element of the carrier of L
(L . Y) "\/" (L . l1) is Element of the carrier of L
Y is Element of the carrier of L
x is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) sups-preserving join-preserving directed-sups-preserving Element of bool [: the carrier of L, the carrier of L:]
bool the carrier of L is non empty set
l1 is Element of the carrier of L
{l1} is non empty trivial finite V44(1) Element of bool the carrier of L
Y is non empty directed Element of bool the carrier of L
"\/" (Y,L) is Element of the carrier of L
l1 "/\" ("\/" (Y,L)) is Element of the carrier of L
{l1} "/\" Y is non empty Element of bool the carrier of L
"\/" (({l1} "/\" Y),L) is Element of the carrier of L
Y is non empty directed Element of bool the carrier of L
Y "/\" Y is non empty directed Element of bool the carrier of L
{l1} "/\" Y is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
L .: Y is non empty Element of bool the carrier of L
dom L is Element of bool the carrier of L
L . l1 is Element of the carrier of L
{(L . l1)} is non empty trivial finite V44(1) Element of bool the carrier of L
{(L . l1)} "/\" (L .: Y) is non empty Element of bool the carrier of L
{ ((L . l1) "/\" b₁) where b₁ is Element of the carrier of L : b₁ in L .: Y } is set
L .: ({l1} "/\" Y) is non empty Element of bool the carrier of L
p is set
f1 is Element of the carrier of L
(L . l1) "/\" f1 is Element of the carrier of L
D is set
L . D is set
f is Element of the carrier of L
l1 "/\" f is Element of the carrier of L
{ (l1 "/\" b₁) where b₁ is Element of the carrier of L : b₁ in Y } is set
{l1,f} is non empty finite Element of bool the carrier of L
L . (l1 "/\" f) is Element of the carrier of L
{ (l1 "/\" b₁) where b₁ is Element of the carrier of L : b₁ in Y } is set
p is set
f1 is set
L . f1 is set
D is Element of the carrier of L
f is Element of the carrier of L
l1 "/\" f is Element of the carrier of L
L . f is Element of the carrier of L
{l1,f} is non empty finite Element of bool the carrier of L
P is Element of the carrier of L
(L . l1) "/\" P is Element of the carrier of L
l1 "/\" ("\/" (Y,L)) is Element of the carrier of L
L . (l1 "/\" ("\/" (Y,L))) is Element of the carrier of L
L . ("\/" (Y,L)) is Element of the carrier of L
(L . l1) "/\" (L . ("\/" (Y,L))) is Element of the carrier of L
x is directed Element of bool the carrier of L
"\/" (x,L) is Element of the carrier of L
(L . l1) "/\" ("\/" (x,L)) is Element of the carrier of L
{(L . l1)} "/\" x is Element of bool the carrier of L
"\/" (({(L . l1)} "/\" x),L) is Element of the carrier of L
"\/" ((L .: ({l1} "/\" Y)),L) is Element of the carrier of L
"\/" (({l1} "/\" Y),L) is Element of the carrier of L
L . ("\/" (({l1} "/\" Y),L)) is Element of the carrier of L
L is non empty V110() reflexive RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is non empty V110() reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is upper Element of bool the carrier of L
L is Element of the carrier of L
waybelow L is directed lower Element of bool the carrier of L
l1 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : b₁ is_way_below L } is set
L is Element of the carrier of L
waybelow L is directed lower Element of bool the carrier of L
l1 is set
{ b₁ where b₁ is Element of the carrier of L : b₁ is_way_below L } is set
Y is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is upper Element of bool the carrier of L
{ (wayabove b₁) where b₁ is Element of the carrier of L : b₁ in L } is set
union { (wayabove b₁) where b₁ is Element of the carrier of L : b₁ in L } is set
L is set
l1 is Element of L
Y is Element of the carrier of L
Y is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : Y is_way_below b₁ } is set
wayabove Y is upper Element of bool the carrier of L
L is set
l1 is set
Y is Element of the carrier of L
wayabove Y is upper Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : Y is_way_below b₁ } is set
Y is Element of the carrier of L
L is Element of the carrier of L
l1 is set
Y is Element of the carrier of L
wayabove Y is upper Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : Y is_way_below b₁ } is set
Y is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L
L is Element of the carrier of L
Bottom L is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
L is Element of the carrier of L
wayabove L is upper Element of bool the carrier of L
bool the carrier of L is non empty set
L is Element of the carrier of L
l1 is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of the carrier of L
L is Element of the carrier of L
wayabove L is upper Element of bool the carrier of L
l1 is non empty Element of bool the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
[:l1,l1:] is non empty Relation-like set
bool [:l1,l1:] is non empty set
Y is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
{ (uparrow b₁) where b₁ is Element of the carrier of L : ex b₂ being ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT st b₁ = (L,l1,Y,b₂) . L } is set
x is set
p is Element of the carrier of L
uparrow p is non empty filtered upper Element of bool the carrier of L
{p} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {p} is non empty upper Element of bool the carrier of L
f1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,f1) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,f1) . L is set
bool (bool the carrier of L) is non empty set
x is Element of bool (bool the carrier of L)
f1 is Element of bool the carrier of L
D is Element of bool the carrier of L
f1 \/ D is Element of bool the carrier of L
f is Element of the carrier of L
uparrow f is non empty filtered upper Element of bool the carrier of L
{f} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {f} is non empty upper Element of bool the carrier of L
P is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,P) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,P) . L is set
P is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,P) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,P) . L is set
R is Element of the carrier of L
uparrow R is non empty filtered upper Element of bool the carrier of L
{R} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {R} is non empty upper Element of bool the carrier of L
R "/\" f is Element of the carrier of L
k1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,k1) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,k1) . L is set
k1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,k1) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,k1) . L is set
p is Element of l1
a is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,a) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,l1,(L,l1,Y,a),p) is Element of the carrier of L
b is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
a + b is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,(a + b)) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,l1,(L,l1,Y,(a + b)),p) is Element of the carrier of L
b + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
a + (b + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,(a + (b + 1))) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,l1,(L,l1,Y,(a + (b + 1))),p) is Element of the carrier of L
Y . (L,l1,l1,(L,l1,Y,(a + b)),p) is set
znk is Element of the carrier of L
dom (L,l1,Y,(a + b)) is Element of bool l1
bool l1 is non empty set
Y * (L,l1,Y,(a + b)) is Relation-like l1 -defined l1 -valued Function-like Element of bool [:l1,l1:]
(Y * (L,l1,Y,(a + b))) . p is set
(a + b) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,((a + b) + 1)) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,l1,(L,l1,Y,((a + b) + 1)),p) is Element of the carrier of L
a + 0 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,(a + 0)) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,l1,(L,l1,Y,(a + 0)),p) is Element of the carrier of L
b is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
a + b is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,(a + b)) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,l1,(L,l1,Y,(a + b)),p) is Element of the carrier of L
a is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() set
k1 + a is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
uparrow (R "/\" f) is non empty filtered upper Element of bool the carrier of L
{(R "/\" f)} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {(R "/\" f)} is non empty upper Element of bool the carrier of L
a is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() set
P + a is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
uparrow (R "/\" f) is non empty filtered upper Element of bool the carrier of L
{(R "/\" f)} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {(R "/\" f)} is non empty upper Element of bool the carrier of L
uparrow (R "/\" f) is non empty filtered upper Element of bool the carrier of L
{(R "/\" f)} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {(R "/\" f)} is non empty upper Element of bool the carrier of L
uparrow (R "/\" f) is non empty filtered upper Element of bool the carrier of L
{(R "/\" f)} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {(R "/\" f)} is non empty upper Element of bool the carrier of L
p is Element of bool the carrier of L
f1 is Element of the carrier of L
uparrow f1 is non empty filtered upper Element of bool the carrier of L
{f1} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {f1} is non empty upper Element of bool the carrier of L
D is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,D) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,D) . L is set
uparrow L is non empty filtered upper Element of bool the carrier of L
{L} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {L} is non empty upper Element of bool the carrier of L
union { (uparrow b₁) where b₁ is Element of the carrier of L : ex b₂ being ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT st b₁ = (L,l1,Y,b₂) . L } is set
f1 is set
D is set
f is Element of the carrier of L
uparrow f is non empty filtered upper Element of bool the carrier of L
{f} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {f} is non empty upper Element of bool the carrier of L
P is Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in P ) } is set
R is Element of the carrier of L
f2 is Element of the carrier of L
D is Element of the carrier of L
f1 is Element of bool the carrier of L
f is set
P is Element of the carrier of L
uparrow P is non empty filtered upper Element of bool the carrier of L
{P} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {P} is non empty upper Element of bool the carrier of L
R is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,R) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,R) . L is set
R is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,R) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,R) . L is set
Y . P is set
f2 is Element of the carrier of L
uparrow f2 is non empty filtered upper Element of bool the carrier of L
{f2} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {f2} is non empty upper Element of bool the carrier of L
dom (L,l1,Y,R) is Element of bool l1
bool l1 is non empty set
Y * (L,l1,Y,R) is Relation-like l1 -defined l1 -valued Function-like Element of bool [:l1,l1:]
(Y * (L,l1,Y,R)) . L is set
R + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,(R + 1)) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,(R + 1)) . L is set
k1 is Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in k1 ) } is set
a is Element of the carrier of L
b is Element of the carrier of L
b is Element of the carrier of L
dom Y is Element of bool l1
field Y is set
dom Y is set
rng Y is set
(dom Y) \/ (rng Y) is set
(L,l1,Y,0) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,0) . L is set
id (field Y) is Relation-like field Y -defined field Y -valued Function-like one-to-one V28( field Y) Element of bool [:(field Y),(field Y):]
[:(field Y),(field Y):] is Relation-like set
bool [:(field Y),(field Y):] is non empty set
(id (field Y)) . L is set
D is Element of bool the carrier of L
f is Element of the carrier of L
uparrow f is non empty filtered upper Element of bool the carrier of L
{f} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {f} is non empty upper Element of bool the carrier of L
P is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,P) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,P) . L is set
D is non empty filtered upper (L) Element of bool the carrier of L
f is set
P is set
f2 is Element of the carrier of L
uparrow f2 is non empty filtered upper Element of bool the carrier of L
{f2} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {f2} is non empty upper Element of bool the carrier of L
k1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT
(L,l1,Y,k1) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]
(L,l1,Y,k1) . L is set
R is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is upper (L) Element of bool the carrier of L
L ` is Element of bool the carrier of L
the carrier of L \ L is set
L is Element of the carrier of L
{ b<sub>1</sub> where b<sub>1</sub> is strongly_connected directed filtered Element of bool the carrier of L : ( b<sub>1</sub> c= L ` & L in b₁ ) } is set
{L} is non empty trivial finite V44(1) Element of bool the carrier of L
Y is set
union Y is set
x is set
p is strongly_connected directed filtered Element of bool the carrier of L
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V28( the carrier of L) reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
x is Element of bool the carrier of L
p is set
f1 is set
[p,f1] is set
{p,f1} is non empty finite set
{p} is non empty trivial finite V44(1) set
{{p,f1},{p}} is non empty finite V41() set
[f1,p] is set
{f1,p} is non empty finite set
{f1} is non empty trivial finite V44(1) set
{{f1,p},{f1}} is non empty finite V41() set
D is set
f is set
R is strongly_connected directed filtered Element of bool the carrier of L
f2 is strongly_connected directed filtered Element of bool the carrier of L
R is strongly_connected directed filtered Element of bool the carrier of L
P is strongly_connected directed filtered Element of bool the carrier of L
f1 is set
D is strongly_connected directed filtered Element of bool the carrier of L
the Element of Y is Element of Y
p is strongly_connected directed filtered Element of bool the carrier of L
D is strongly_connected directed filtered Element of bool the carrier of L
Y is strongly_connected directed filtered Element of bool the carrier of L
Y is set
x is strongly_connected directed filtered Element of bool the carrier of L
"\/" (x,L) is Element of the carrier of L
f1 is Element of the carrier of L
{f1} is non empty trivial finite V44(1) Element of bool the carrier of L
x \/ {f1} is non empty Element of bool the carrier of L
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V28( the carrier of L) reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
f is set
P is set
[f,P] is set
{f,P} is non empty finite set
{f} is non empty trivial finite V44(1) set
{{f,P},{f}} is non empty finite V41() set
[P,f] is set
{P,f} is non empty finite set
{P} is non empty trivial finite V44(1) set
{{P,f},{P}} is non empty finite V41() set
f2 is Element of the carrier of L
R is Element of the carrier of L
f2 is Element of the carrier of L
R is Element of the carrier of L
R is Element of the carrier of L
f is strongly_connected directed filtered Element of bool the carrier of L
f1 is Element of the carrier of L
D is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
L is non empty RelStr
the carrier of L is non empty set
L is non empty RelStr
the carrier of L is non empty set
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of bool the carrier of L
L is Element of the carrier of L
l1 is Element of the carrier of L
L is Element of bool the carrier of L
L is Element of bool the carrier of L
l1 is set
Y is Element of the carrier of L
l1 is set
Y is Element of the carrier of L
L is non empty antisymmetric upper-bounded with_infima RelStr
Top L is Element of the carrier of L
the carrier of L is non empty set
L is Element of the carrier of L
L is Element of the carrier of L
L "/\" L is Element of the carrier of L
L "/\" L is Element of the carrier of L
L is non empty antisymmetric upper-bounded with_infima RelStr
the carrier of L is non empty set
Top L is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of the carrier of L
L is non empty finite Element of bool the carrier of L
"/\" (L,L) is Element of the carrier of L
l1 is set
Y is set
"/\" (Y,L) is Element of the carrier of L
{l1} is non empty trivial finite V44(1) set
Y \/ {l1} is non empty set
"/\" ((Y \/ {l1}),L) is Element of the carrier of L
Y is Element of the carrier of L
{Y} is non empty trivial finite V44(1) Element of bool the carrier of L
Y \/ {Y} is non empty set
"/\" ((Y \/ {Y}),L) is Element of the carrier of L
Y is Element of the carrier of L
{Y} is non empty trivial finite V44(1) Element of bool the carrier of L
"/\" ({Y},L) is Element of the carrier of L
x is finite Element of bool the carrier of L
"/\" (x,L) is Element of the carrier of L
("/\" (x,L)) "/\" ("/\" ({Y},L)) is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
L is Element of the carrier of L
l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
{L,l1} is non empty finite Element of bool the carrier of L
"/\" ({L,l1},L) is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of the carrier of L
uparrow L is non empty filtered upper Element of bool the carrier of L
{L} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {L} is non empty upper Element of bool the carrier of L
(uparrow L) \ {L} is Element of bool the carrier of L
l1 is Element of the carrier of L
Y is Element of the carrier of L
l1 "/\" Y is Element of the carrier of L
Y is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of the carrier of L
L is non empty filtered upper Element of bool the carrier of L
L ` is Element of bool the carrier of L
the carrier of L \ L is set
the carrier of L \ L is Element of bool the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
Y "/\" Y is Element of the carrier of L
x is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
L is Element of the carrier of L
L is Element of the carrier of L
l1 is Element of the carrier of L
waybelow l1 is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
Y is Element of the carrier of L
waybelow Y is non empty directed lower Element of bool the carrier of L
l1 is Element of the carrier of L
bool the carrier of L is non empty set
wayabove l1 is upper Element of bool the carrier of L
Y is non empty filtered upper (L) Element of bool the carrier of L
uparrow l1 is non empty filtered upper Element of bool the carrier of L
{l1} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {l1} is non empty upper Element of bool the carrier of L
the carrier of L \ Y is Element of bool the carrier of L
Y ` is Element of bool the carrier of L
the carrier of L \ Y is set
Y is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of bool the carrier of L
bool L is non empty set
L is Element of the carrier of L
uparrow L is non empty filtered upper Element of bool the carrier of L
{L} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {L} is non empty upper Element of bool the carrier of L
(uparrow L) /\ L is Element of bool the carrier of L
l1 is set
l1 is Element of bool L
"/\" (l1,L) is Element of the carrier of L
L is Element of the carrier of L
uparrow L is non empty filtered upper Element of bool the carrier of L
{L} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {L} is non empty upper Element of bool the carrier of L
(uparrow L) /\ L is Element of bool the carrier of L
"/\" (((uparrow L) /\ L),L) is Element of the carrier of L
l1 is Element of bool L
"/\" (l1,L) is Element of the carrier of L
Y is Element of the carrier of L
x is Element of the carrier of L
Y is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of bool the carrier of L
L is Element of bool the carrier of L
bool L is non empty set
l1 is set
Y is Element of the carrier of L
uparrow Y is non empty filtered upper Element of bool the carrier of L
{Y} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {Y} is non empty upper Element of bool the carrier of L
(uparrow Y) /\ L is Element of bool the carrier of L
(uparrow Y) /\ L is Element of bool the carrier of L
"/\" (((uparrow Y) /\ L),L) is Element of the carrier of L
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ c= L } is set
l1 is set
Y is Element of bool the carrier of L
"/\" (Y,L) is Element of the carrier of L
Y is set
Y is Element of the carrier of L
{Y} is non empty trivial finite V44(1) Element of bool the carrier of L
x is Element of bool the carrier of L
"/\" (x,L) is Element of the carrier of L
l1 is Element of bool the carrier of L
bool L is non empty set
Y is Element of the carrier of L
bool l1 is non empty set
Y is Element of bool l1
"/\" (Y,L) is Element of the carrier of L
{ b₁ where b₁ is Element of bool the carrier of L : ( b₁ c= L & "/\" (b₁,L) in Y ) } is set
union { b₁ where b₁ is Element of bool the carrier of L : ( b₁ c= L & "/\" (b₁,L) in Y ) } is set
p is set
f1 is set
D is Element of bool the carrier of L
"/\" (D,L) is Element of the carrier of L
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : S₁[b₁] } is set
D is set
f is Element of bool the carrier of L
"/\" (f,L) is Element of the carrier of L
D is set
f is Element of bool the carrier of L
"/\" (f,L) is Element of the carrier of L
p is Element of bool the carrier of L
D is set
f is Element of bool the carrier of L
"/\" (f,L) is Element of the carrier of L
"/\" ( { ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : S₁[b₁] } ,L) is Element of the carrier of L
{ b₁ where b₁ is Element of bool the carrier of L : S₁[b₁] } is set
union { b₁ where b₁ is Element of bool the carrier of L : S₁[b₁] } is set
"/\" ((union { b₁ where b₁ is Element of bool the carrier of L : S₁[b₁] } ),L) is Element of the carrier of L
Y is Element of bool the carrier of L
"/\" (Y,L) is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of bool the carrier of L
l1 is Element of the carrier of L
L is Element of the carrier of L
bool L is non empty set
Y is Element of bool L
"/\" (Y,L) is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
L is Element of the carrier of L
uparrow L is non empty filtered upper Element of bool the carrier of L
{L} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {L} is non empty upper Element of bool the carrier of L
(uparrow L) /\ L is Element of bool the carrier of L
"/\" (((uparrow L) /\ L),L) is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
(L) is Element of bool the carrier of L
Top L is Element of the carrier of L
{(Top L)} is non empty trivial finite V44(1) Element of bool the carrier of L
(L) \ {(Top L)} is Element of bool the carrier of L
L is Element of bool the carrier of L
l1 is Element of the carrier of L
L is Element of the carrier of L
Y is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of bool the carrier of L
L is Element of bool the carrier of L
l1 is Element of the carrier of L
uparrow l1 is non empty filtered upper Element of bool the carrier of L
{l1} is non empty trivial finite V44(1) Element of bool the carrier of L
uparrow {l1} is non empty upper Element of bool the carrier of L
(uparrow l1) /\ L is Element of bool the carrier of L
"/\" (((uparrow l1) /\ L),L) is Element of the carrier of L
"/\" ((uparrow l1),L) is Element of the carrier of L
(uparrow l1) /\ L is Element of bool the carrier of L
"/\" (((uparrow l1) /\ L),L) is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of bool the carrier of L
L is Element of the carrier of L
l1 is Element of the carrier of L
L is Element of bool the carrier of L
L is Element of bool the carrier of L
l1 is set
Y is Element of the carrier of L
l1 is set
Y is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
L is non empty antisymmetric upper-bounded RelStr
Top L is Element of the carrier of L
the carrier of L is non empty set
L is Element of the carrier of L
L is Element of the carrier of L
L "/\" L is Element of the carrier of L
L is non empty antisymmetric lower-bounded RelStr
Bottom L is Element of the carrier of L
the carrier of L is non empty set
L ~ is non empty strict antisymmetric upper-bounded RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
RelStr(# the carrier of L,( the InternalRel of L ~) #) is non empty strict RelStr
Top (L ~) is Element of the carrier of (L ~)
the carrier of (L ~) is non empty set
(Bottom L) ~ is Element of the carrier of (L ~)
L is non empty antisymmetric upper-bounded RelStr
the carrier of L is non empty set
Top L is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of the carrier of L
L is non empty finite Element of bool the carrier of L
"/\" (L,L) is Element of the carrier of L
l1 is set
Y is set
"/\" (Y,L) is Element of the carrier of L
{l1} is non empty trivial finite V44(1) set
Y \/ {l1} is non empty set
"/\" ((Y \/ {l1}),L) is Element of the carrier of L
Y is Element of the carrier of L
{Y} is non empty trivial finite V44(1) Element of bool the carrier of L
Y \/ {Y} is non empty set
"/\" ((Y \/ {Y}),L) is Element of the carrier of L
Y is Element of the carrier of L
{Y} is non empty trivial finite V44(1) Element of bool the carrier of L
"/\" ({Y},L) is Element of the carrier of L
x is finite Element of bool the carrier of L
"/\" (x,L) is Element of the carrier of L
("/\" (x,L)) "/\" ("/\" ({Y},L)) is Element of the carrier of L
p is Element of the carrier of L
p is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
l1 is Element of the carrier of L
L is Element of the carrier of L
l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
{L,l1} is non empty finite Element of bool the carrier of L
"/\" ({L,l1},L) is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
Y is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is Element of the carrier of L
L ~ is non empty strict V110() reflexive transitive antisymmetric with_infima RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V28( the carrier of L) reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
RelStr(# the carrier of L,( the InternalRel of L ~) #) is non empty strict RelStr
L ~ is Element of the carrier of (L ~)
the carrier of (L ~) is non empty set
L is non empty finite Element of bool the carrier of L
"\/" (L,L) is Element of the carrier of L
bool the carrier of (L ~) is non empty set
("\/" (L,L)) ~ is Element of the carrier of (L ~)
Y is Element of the carrier of (L ~)
~ Y is Element of the carrier of L
l1 is non empty finite Element of bool the carrier of (L ~)
"/\" (l1,(L ~)) is Element of the carrier of (L ~)
Y is Element of the carrier of (L ~)
~ Y is Element of the carrier of L
L ~ is non empty strict V110() reflexive transitive antisymmetric with_infima RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V28( the carrier of L) reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
RelStr(# the carrier of L,( the InternalRel of L ~) #) is non empty strict RelStr
the carrier of (L ~) is non empty set
L is Element of the carrier of (L ~)
~ L is Element of the carrier of L
l1 is Element of the carrier of (L ~)
~ l1 is Element of the carrier of L
{(~ L),(~ l1)} is non empty finite Element of bool the carrier of L
L "/\" l1 is Element of the carrier of (L ~)
L ~ is Element of the carrier of (L ~)
~ (L "/\" l1) is Element of the carrier of L
"\/" ({(~ L),(~ l1)},L) is Element of the carrier of L
(~ L) "\/" (~ l1) is Element of the carrier of L
Y is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
L is Element of the carrier of L
L is Element of the carrier of L
l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
L is Element of the carrier of L
L is set
{L} is non empty trivial finite V44(1) set
BoolePoset {L} is non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive Heyting complemented Boolean with_suprema with_infima complete satisfying_MC meet-continuous RelStr
the carrier of (BoolePoset {L}) is non empty set
[: the carrier of L, the carrier of (BoolePoset {L}):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (BoolePoset {L}):] is non empty set
l1 is Relation-like the carrier of L -defined the carrier of (BoolePoset {L}) -valued Function-like V32( the carrier of L, the carrier of (BoolePoset {L})) Element of bool [: the carrier of L, the carrier of (BoolePoset {L}):]
bool {L} is non empty finite V41() set
InclPoset (bool {L}) is non empty strict V110() reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (bool {L})) is non empty set
{{},{L}} is non empty finite V41() set
dom l1 is Element of bool the carrier of L
bool the carrier of L is non empty set
Y is Element of the carrier of L
Y is Element of the carrier of L
{Y,Y} is non empty finite Element of bool the carrier of L
l1 .: {Y,Y} is non empty finite Element of bool the carrier of (BoolePoset {L})
bool the carrier of (BoolePoset {L}) is non empty set
l1 . Y is Element of the carrier of (BoolePoset {L})
l1 . Y is Element of the carrier of (BoolePoset {L})
{(l1 . Y),(l1 . Y)} is non empty finite Element of bool the carrier of (BoolePoset {L})
Y "/\" Y is Element of the carrier of L
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})
{} /\ {} is Relation-like finite set
l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})
Y "/\" Y is Element of the carrier of L
l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})
{L} /\ {L} is finite set
Y "/\" Y is Element of the carrier of L
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})
{} /\ {L} is Relation-like finite set
l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})
Y "/\" Y is Element of the carrier of L
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})
{L} /\ {} is Relation-like finite set
l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})
Y "/\" Y is Element of the carrier of L
l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})
Y "/\" Y is Element of the carrier of L
l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})
"/\" ((l1 .: {Y,Y}),(BoolePoset {L})) is Element of the carrier of (BoolePoset {L})
"/\" ({Y,Y},L) is Element of the carrier of L
l1 . ("/\" ({Y,Y},L)) is Element of the carrier of (BoolePoset {L})
Y is Element of the carrier of L
Y is Element of the carrier of L
{Y,Y} is non empty finite Element of bool the carrier of L
l1 .: {Y,Y} is non empty finite Element of bool the carrier of (BoolePoset {L})
bool the carrier of (BoolePoset {L}) is non empty set
l1 . Y is Element of the carrier of (BoolePoset {L})
l1 . Y is Element of the carrier of (BoolePoset {L})
{(l1 . Y),(l1 . Y)} is non empty finite Element of bool the carrier of (BoolePoset {L})
Y "\/" Y is Element of the carrier of L
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})
{} \/ {} is Relation-like finite V41() set
l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})
Y "\/" Y is Element of the carrier of L
l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})
{L} \/ {L} is non empty finite set
Y "\/" Y is Element of the carrier of L
l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})
{} \/ {L} is non empty finite set
Y "\/" Y is Element of the carrier of L
l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})
{L} \/ {} is non empty finite set
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})
Y "\/" Y is Element of the carrier of L
l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})
Y "\/" Y is Element of the carrier of L
l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})
"\/" ((l1 .: {Y,Y}),(BoolePoset {L})) is Element of the carrier of (BoolePoset {L})
"\/" ({Y,Y},L) is Element of the carrier of L
l1 . ("\/" ({Y,Y},L)) is Element of the carrier of (BoolePoset {L})
L is Element of the carrier of L
l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
BoolePoset {{}} is non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive Heyting complemented Boolean with_suprema with_infima complete satisfying_MC meet-continuous RelStr
the carrier of (BoolePoset {{}}) is non empty set
bool {{}} is non empty finite V41() set
InclPoset (bool {{}}) is non empty strict V110() reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (bool {{}})) is non empty set
{{},{{}}} is non empty finite V41() set
Y is Element of the carrier of L
x is Element of the carrier of (BoolePoset {{}})
x is Element of the carrier of (BoolePoset {{}})
Y is Element of the carrier of (BoolePoset {{}})
[: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty set
Y is Relation-like the carrier of L -defined the carrier of (BoolePoset {{}}) -valued Function-like V32( the carrier of L, the carrier of (BoolePoset {{}})) Element of bool [: the carrier of L, the carrier of (BoolePoset {{}}):]
{L,l1} is non empty finite Element of bool the carrier of L
bool the carrier of L is non empty set
dom Y is Element of bool the carrier of L
Y .: {L,l1} is non empty finite Element of bool the carrier of (BoolePoset {{}})
bool the carrier of (BoolePoset {{}}) is non empty set
Y . L is Element of the carrier of (BoolePoset {{}})
Y . l1 is Element of the carrier of (BoolePoset {{}})
{(Y . L),(Y . l1)} is non empty finite Element of bool the carrier of (BoolePoset {{}})
L "/\" l1 is Element of the carrier of L
Y . (L "/\" l1) is Element of the carrier of (BoolePoset {{}})
"/\" ({L,l1},L) is Element of the carrier of L
Y . ("/\" ({L,l1},L)) is Element of the carrier of (BoolePoset {{}})
"/\" ({(Y . L),(Y . l1)},(BoolePoset {{}})) is Element of the carrier of (BoolePoset {{}})
(Y . L) "/\" (Y . l1) is Element of the carrier of (BoolePoset {{}})
(Y . L) /\ (Y . l1) is set
L is non empty V110() reflexive transitive antisymmetric upper-bounded with_suprema with_infima RelStr
the carrier of L is non empty set
Top L is Element of the carrier of L
bool the carrier of L is non empty set
L is Element of the carrier of L
downarrow L is non empty directed lower Element of bool the carrier of L
{L} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {L} is non empty lower Element of bool the carrier of L
(downarrow L) ` is Element of bool the carrier of L
the carrier of L \ (downarrow L) is set
the carrier of L \ (downarrow L) is Element of bool the carrier of L
Y is Element of the carrier of L
l1 is Element of bool the carrier of L
Y is Element of the carrier of L
Y "/\" Y is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
Y "/\" Y is Element of the carrier of L
Y "/\" Y is Element of the carrier of L
l1 is Element of bool the carrier of L
x is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric distributive with_suprema with_infima RelStr
the carrier of L is non empty set
L is Element of the carrier of L
L is Element of the carrier of L
l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
L "\/" (L "/\" l1) is Element of the carrier of L
L "\/" L is Element of the carrier of L
L "\/" l1 is Element of the carrier of L
(L "\/" L) "/\" (L "\/" l1) is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric distributive with_suprema with_infima RelStr
(L) is Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
(L) is Element of bool the carrier of L
L is set
L is Element of (L)
l1 is Element of the carrier of L
L is set
L is Element of (L)
l1 is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() distributive Heyting complemented Boolean with_suprema with_infima RelStr
the carrier of L is non empty set
Top L is Element of the carrier of L
L is Element of the carrier of L
L is Element of the carrier of L
l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
Bottom L is Element of the carrier of L
L "\/" l1 is Element of the carrier of L
L is Element of the carrier of L
l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
L "/\" l1 is Element of the carrier of L
L "\/" (L "/\" l1) is Element of the carrier of L
L "\/" L is Element of the carrier of L
L "\/" l1 is Element of the carrier of L
(L "\/" L) "/\" (L "\/" l1) is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
Top L is Element of the carrier of L
bool the carrier of L is non empty set
L is Element of the carrier of L
downarrow L is non empty directed lower Element of bool the carrier of L
{L} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {L} is non empty lower Element of bool the carrier of L
(downarrow L) ` is Element of bool the carrier of L
the carrier of L \ (downarrow L) is set
l1 is Element of the carrier of L
waybelow l1 is non empty directed lower Element of bool the carrier of L
Y is Element of the carrier of L
waybelow Y is non empty directed lower Element of bool the carrier of L
l1 is Element of the carrier of L
Y is Element of the carrier of L
l1 is non empty filtered upper (L) Element of bool the carrier of L
l1 ` is Element of bool the carrier of L
the carrier of L \ l1 is set
Y is Element of the carrier of L
l1 is non empty filtered upper (L) Element of bool the carrier of L
l1 ` is Element of bool the carrier of L
the carrier of L \ l1 is set
l1 is Element of the carrier of L
Y is Element of the carrier of L
l1 "/\" Y is Element of the carrier of L
L "\/" (l1 "/\" Y) is Element of the carrier of L
L "\/" l1 is Element of the carrier of L
L "\/" Y is Element of the carrier of L
(L "\/" l1) "/\" (L "\/" Y) is Element of the carrier of L
BoolePoset {{}} is non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive Heyting complemented Boolean with_suprema with_infima complete satisfying_MC meet-continuous RelStr
the carrier of (BoolePoset {{}}) is non empty set
L is RelStr
the carrier of L is set
bool the carrier of L is non empty set
[: the carrier of L, the carrier of (BoolePoset {{}}):] is Relation-like set
bool [: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty set
L is Element of bool the carrier of L
chi (L, the carrier of L) is Relation-like the carrier of L -defined {{},1} -valued Function-like V32( the carrier of L,{{},1}) Element of bool [: the carrier of L,{{},1}:]
[: the carrier of L,{{},1}:] is Relation-like set
bool [: the carrier of L,{{},1}:] is non empty set
bool {{}} is non empty finite V41() set
InclPoset (bool {{}}) is non empty strict V110() reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (bool {{}})) is non empty set
{0,1} is non empty finite V41() Element of bool NAT
L is non empty RelStr
the carrier of L is non empty set
L is Element of the carrier of L
downarrow L is Element of bool the carrier of L
bool the carrier of L is non empty set
{L} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {L} is Element of bool the carrier of L
(downarrow L) ` is Element of bool the carrier of L
the carrier of L \ (downarrow L) is set
chi (((downarrow L) `), the carrier of L) is Relation-like the carrier of L -defined {{},1} -valued Function-like V32( the carrier of L,{{},1}) Element of bool [: the carrier of L,{{},1}:]
[: the carrier of L,{{},1}:] is non empty Relation-like set
bool [: the carrier of L,{{},1}:] is non empty set
L is Element of the carrier of L
(chi (((downarrow L) `), the carrier of L)) . L is finite Element of {{},1}
L is non empty V110() reflexive transitive antisymmetric upper-bounded with_suprema with_infima RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty set
L is Relation-like the carrier of L -defined the carrier of (BoolePoset {{}}) -valued Function-like V32( the carrier of L, the carrier of (BoolePoset {{}})) Element of bool [: the carrier of L, the carrier of (BoolePoset {{}}):]
L is (L) Element of the carrier of L
downarrow L is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{L} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {L} is non empty lower Element of bool the carrier of L
(downarrow L) ` is Element of bool the carrier of L
the carrier of L \ (downarrow L) is set
chi (((downarrow L) `), the carrier of L) is Relation-like the carrier of L -defined {{},1} -valued Function-like V32( the carrier of L,{{},1}) Element of bool [: the carrier of L,{{},1}:]
[: the carrier of L,{{},1}:] is non empty Relation-like set
bool [: the carrier of L,{{},1}:] is non empty set
l1 is Element of the carrier of L
L . l1 is Element of the carrier of (BoolePoset {{}})
Y is Element of the carrier of L
L . Y is Element of the carrier of (BoolePoset {{}})
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
(L) is Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
{ (chi (((downarrow b<sub>1</sub>) `), the carrier of L)) where b₁ is Element of the carrier of L : b₁ is (L) } is set
the (L) Element of the carrier of L is (L) Element of the carrier of L
downarrow the (L) Element of the carrier of L is non empty directed lower Element of bool the carrier of L
{ the (L) Element of the carrier of L} is non