:: 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 empty trivial finite V44(1) Element of bool the carrier of L
downarrow { the (L) Element of the carrier of L} is non empty lower Element of bool the carrier of L
(downarrow the (L) Element of the carrier of L) ` is Element of bool the carrier of L
the carrier of L \ (downarrow the (L) Element of the carrier of L) is set
chi (((downarrow the (L) Element of the carrier of 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 set
Y is Element of the carrier of L
downarrow Y is non empty directed lower Element of bool the carrier of L
{Y} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {Y} is non empty lower Element of bool the carrier of L
(downarrow Y) ` is Element of bool the carrier of L
the carrier of L \ (downarrow Y) is set
chi (((downarrow Y) `), 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}:]
l1 is non empty functional set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . a₁ = 1 } is set
Y is Relation-like Function-like set
dom Y is set
BoolePoset l1 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 l1) is non empty set
bool l1 is non empty set
InclPoset (bool l1) is non empty strict V110() reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (bool l1)) is non empty set
rng Y is set
Y is set
x is set
Y . x is set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . x = 1 } is set
p is set
f1 is Relation-like Function-like Element of l1
f1 . x is set
[: the carrier of L, the carrier of (BoolePoset l1):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (BoolePoset l1):] is non empty set
Y is Relation-like the carrier of L -defined the carrier of (BoolePoset l1) -valued Function-like V32( the carrier of L, the carrier of (BoolePoset l1)) Element of bool [: the carrier of L, the carrier of (BoolePoset l1):]
x is Element of the carrier of L
p is Element of the carrier of L
{x,p} is non empty finite Element of bool the carrier of L
Y .: {x,p} is non empty finite Element of bool the carrier of (BoolePoset l1)
bool the carrier of (BoolePoset l1) is non empty set
"/\" ((Y .: {x,p}),(BoolePoset l1)) is Element of the carrier of (BoolePoset l1)
"/\" ({x,p},L) is Element of the carrier of L
Y . ("/\" ({x,p},L)) is Element of the carrier of (BoolePoset l1)
x "/\" p is Element of the carrier of L
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . (x "/\" p) = 1 } is set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . x = 1 } is set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . p = 1 } is set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . x = 1 } /\ { b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . p = 1 } is set
f1 is set
Top (BoolePoset {{}}) is Element of the carrier of (BoolePoset {{}})
D is Relation-like Function-like Element of l1
D . (x "/\" p) is 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
P is Element of the carrier of L
downarrow P is non empty directed lower Element of bool the carrier of L
{P} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {P} is non empty lower Element of bool the carrier of L
(downarrow P) ` is Element of bool the carrier of L
the carrier of L \ (downarrow P) is set
chi (((downarrow P) `), 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}:]
f 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 {{}}):]
P is Element of the carrier of L
downarrow P is non empty directed lower Element of bool the carrier of L
{P} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {P} is non empty lower Element of bool the carrier of L
(downarrow P) ` is Element of bool the carrier of L
the carrier of L \ (downarrow P) is set
chi (((downarrow P) `), 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}:]
dom f is Element of bool the carrier of L
f . x is Element of the carrier of (BoolePoset {{}})
f . p is Element of the carrier of (BoolePoset {{}})
{(f . x),(f . p)} is non empty finite Element of bool the carrier of (BoolePoset {{}})
bool the carrier of (BoolePoset {{}}) is non empty set
f .: {x,p} is non empty finite Element of bool the carrier of (BoolePoset {{}})
(f . x) "/\" (f . p) is Element of the carrier of (BoolePoset {{}})
"/\" ({(f . x),(f . p)},(BoolePoset {{}})) is Element of the carrier of (BoolePoset {{}})
f . (x "/\" p) is Element of the carrier of (BoolePoset {{}})
f1 is set
D is Relation-like Function-like Element of l1
D . x is set
f is Element of the carrier of L
downarrow f is non empty directed lower Element of bool the carrier of L
{f} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {f} is non empty lower Element of bool the carrier of L
(downarrow f) ` is Element of bool the carrier of L
the carrier of L \ (downarrow f) is set
chi (((downarrow f) `), 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, the carrier of (BoolePoset {{}}):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty set
P 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 {{}}):]
R is Element of the carrier of L
P . R is Element of the carrier of (BoolePoset {{}})
f2 is Element of the carrier of L
P . f2 is Element of the carrier of (BoolePoset {{}})
dom P is Element of bool the carrier of L
P . x is Element of the carrier of (BoolePoset {{}})
P . p is Element of the carrier of (BoolePoset {{}})
{(P . x),(P . p)} is non empty finite Element of bool the carrier of (BoolePoset {{}})
bool the carrier of (BoolePoset {{}}) is non empty set
P .: {x,p} is non empty finite Element of bool the carrier of (BoolePoset {{}})
(P . x) "/\" (P . p) is Element of the carrier of (BoolePoset {{}})
"/\" ({(P . x),(P . p)},(BoolePoset {{}})) is Element of the carrier of (BoolePoset {{}})
P . (x "/\" p) is Element of the carrier of (BoolePoset {{}})
R is Relation-like Function-like Element of l1
R . p is set
Y . x is Element of the carrier of (BoolePoset l1)
Y . p is Element of the carrier of (BoolePoset l1)
{(Y . x),(Y . p)} is non empty finite Element of bool the carrier of (BoolePoset l1)
(Y . x) "/\" (Y . p) is Element of the carrier of (BoolePoset l1)
(Y . x) /\ (Y . p) is set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . x = 1 } /\ (Y . p) is set
Y . (x "/\" p) is Element of the carrier of (BoolePoset l1)
x is set
dom Y is set
p is set
Y . x is set
Y . p is set
dom Y is Element of bool the carrier of L
f1 is Element of the carrier of L
Y . f1 is Element of the carrier of (BoolePoset l1)
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . f1 = 1 } is set
D is Element of the carrier of L
Y . D is Element of the carrier of (BoolePoset l1)
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . D = 1 } is set
f is Element of the carrier of L
downarrow f is non empty directed lower Element of bool the carrier of L
{f} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {f} is non empty lower Element of bool the carrier of L
(downarrow f) ` is Element of bool the carrier of L
the carrier of L \ (downarrow f) is set
chi (((downarrow f) `), 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}:]
R is Relation-like Function-like Element of l1
f2 is Relation-like Function-like Element of l1
f2 . f1 is set
dom R is set
rng R is set
{0,1} is non empty finite V41() Element of bool NAT
R . D is set
f is Element of the carrier of L
downarrow f is non empty directed lower Element of bool the carrier of L
{f} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {f} is non empty lower Element of bool the carrier of L
(downarrow f) ` is Element of bool the carrier of L
the carrier of L \ (downarrow f) is set
chi (((downarrow f) `), 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}:]
R is Relation-like Function-like Element of l1
f2 is Relation-like Function-like Element of l1
f2 . D is set
dom R is set
rng R is set
{0,1} is non empty finite V41() Element of bool NAT
R . f1 is set
x is Element of the carrier of L
p is Element of the carrier of L
{x,p} is non empty finite Element of bool the carrier of L
Y .: {x,p} is non empty finite Element of bool the carrier of (BoolePoset l1)
bool the carrier of (BoolePoset l1) is non empty set
"\/" ((Y .: {x,p}),(BoolePoset l1)) is Element of the carrier of (BoolePoset l1)
"\/" ({x,p},L) is Element of the carrier of L
Y . ("\/" ({x,p},L)) is Element of the carrier of (BoolePoset l1)
x "\/" p is Element of the carrier of L
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . (x "\/" p) = 1 } is set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . x = 1 } is set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . p = 1 } is set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . x = 1 } \/ { b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . p = 1 } is set
f1 is set
Top (BoolePoset {{}}) is Element of the carrier of (BoolePoset {{}})
D is Relation-like Function-like Element of l1
D . (x "\/" p) is 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
P is Element of the carrier of L
downarrow P is non empty directed lower Element of bool the carrier of L
{P} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {P} is non empty lower Element of bool the carrier of L
(downarrow P) ` is Element of bool the carrier of L
the carrier of L \ (downarrow P) is set
chi (((downarrow P) `), 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}:]
f 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 {{}}):]
P is Element of the carrier of L
downarrow P is non empty directed lower Element of bool the carrier of L
{P} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {P} is non empty lower Element of bool the carrier of L
(downarrow P) ` is Element of bool the carrier of L
the carrier of L \ (downarrow P) is set
chi (((downarrow P) `), 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}:]
dom f is Element of bool the carrier of L
f .: {x,p} is non empty finite Element of bool the carrier of (BoolePoset {{}})
bool the carrier of (BoolePoset {{}}) is non empty set
f . x is Element of the carrier of (BoolePoset {{}})
f . p is Element of the carrier of (BoolePoset {{}})
{(f . x),(f . p)} is non empty finite Element of bool the carrier of (BoolePoset {{}})
(f . x) "\/" (f . p) is Element of the carrier of (BoolePoset {{}})
"\/" ({(f . x),(f . p)},(BoolePoset {{}})) is Element of the carrier of (BoolePoset {{}})
{} \/ {} is Relation-like finite V41() 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
f1 is set
D is Relation-like Function-like Element of l1
D . x is set
f is Element of the carrier of L
downarrow f is non empty directed lower Element of bool the carrier of L
{f} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {f} is non empty lower Element of bool the carrier of L
(downarrow f) ` is Element of bool the carrier of L
the carrier of L \ (downarrow f) is set
chi (((downarrow f) `), 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, the carrier of (BoolePoset {{}}):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty set
P 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 {{}}):]
R is Element of the carrier of L
P . R is Element of the carrier of (BoolePoset {{}})
f2 is Element of the carrier of L
P . f2 is Element of the carrier of (BoolePoset {{}})
dom P is Element of bool the carrier of L
P . x is Element of the carrier of (BoolePoset {{}})
P . p is Element of the carrier of (BoolePoset {{}})
{(P . x),(P . p)} is non empty finite Element of bool the carrier of (BoolePoset {{}})
bool the carrier of (BoolePoset {{}}) is non empty set
P .: {x,p} is non empty finite Element of bool the carrier of (BoolePoset {{}})
Top (BoolePoset {{}}) is Element of the carrier of (BoolePoset {{}})
(P . x) "\/" (P . p) is Element of the carrier of (BoolePoset {{}})
"\/" ({(P . x),(P . p)},(BoolePoset {{}})) is Element of the carrier of (BoolePoset {{}})
P . (x "\/" p) is Element of the carrier of (BoolePoset {{}})
D is Relation-like Function-like Element of l1
D . p is set
f is Element of the carrier of L
downarrow f is non empty directed lower Element of bool the carrier of L
{f} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {f} is non empty lower Element of bool the carrier of L
(downarrow f) ` is Element of bool the carrier of L
the carrier of L \ (downarrow f) is set
chi (((downarrow f) `), 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, the carrier of (BoolePoset {{}}):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty set
P 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 {{}}):]
R is Element of the carrier of L
P . R is Element of the carrier of (BoolePoset {{}})
f2 is Element of the carrier of L
P . f2 is Element of the carrier of (BoolePoset {{}})
dom P is Element of bool the carrier of L
P . x is Element of the carrier of (BoolePoset {{}})
P . p is Element of the carrier of (BoolePoset {{}})
{(P . x),(P . p)} is non empty finite Element of bool the carrier of (BoolePoset {{}})
bool the carrier of (BoolePoset {{}}) is non empty set
P .: {x,p} is non empty finite Element of bool the carrier of (BoolePoset {{}})
Top (BoolePoset {{}}) is Element of the carrier of (BoolePoset {{}})
(P . x) "\/" (P . p) is Element of the carrier of (BoolePoset {{}})
"\/" ({(P . x),(P . p)},(BoolePoset {{}})) is Element of the carrier of (BoolePoset {{}})
P . (x "\/" p) is Element of the carrier of (BoolePoset {{}})
(P . p) "\/" (P . x) is Element of the carrier of (BoolePoset {{}})
Y . x is Element of the carrier of (BoolePoset l1)
Y . p is Element of the carrier of (BoolePoset l1)
{(Y . x),(Y . p)} is non empty finite Element of bool the carrier of (BoolePoset l1)
(Y . x) "\/" (Y . p) is Element of the carrier of (BoolePoset l1)
(Y . x) \/ (Y . p) is set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . x = 1 } \/ (Y . p) is set
Y . (x "\/" p) is Element of the carrier of (BoolePoset l1)
x is Element of bool the carrier of L
Y .: x is Element of bool the carrier of (BoolePoset l1)
bool the carrier of (BoolePoset l1) is non empty set
"\/" ((Y .: x),(BoolePoset l1)) is Element of the carrier of (BoolePoset l1)
"\/" (x,L) is Element of the carrier of L
Y . ("\/" (x,L)) is Element of the carrier of (BoolePoset l1)
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . ("\/" (x,L)) = 1 } is set
p is set
union (Y .: x) is set
f1 is set
dom Y is Element of bool the carrier of L
D is set
Y . D is set
f is Element of the carrier of L
Y . f is Element of the carrier of (BoolePoset l1)
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . f = 1 } is set
P is Relation-like Function-like Element of l1
P . f is set
R is Element of the carrier of L
downarrow R is non empty directed lower Element of bool the carrier of L
{R} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {R} is non empty lower Element of bool the carrier of L
(downarrow R) ` is Element of bool the carrier of L
the carrier of L \ (downarrow R) is set
chi (((downarrow R) `), 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}:]
P . ("\/" (x,L)) is set
dom P is set
rng P is set
{0,1} is non empty finite V41() Element of bool NAT
p is set
f1 is Relation-like Function-like Element of l1
f1 . ("\/" (x,L)) is set
D is Element of the carrier of L
downarrow D is non empty directed lower Element of bool the carrier of L
{D} is non empty trivial finite V44(1) Element of bool the carrier of L
downarrow {D} is non empty lower Element of bool the carrier of L
(downarrow D) ` is Element of bool the carrier of L
the carrier of L \ (downarrow D) is set
chi (((downarrow D) `), 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}:]
rng f1 is set
{0,1} is non empty finite V41() Element of bool NAT
f is Element of the carrier of L
f is Element of the carrier of L
dom f1 is set
f1 . f is set
{ b₁ where b₁ is Relation-like Function-like Element of l1 : b₁ . f = 1 } is set
Y . f is Element of the carrier of (BoolePoset l1)
union (Y .: x) is set
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
(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
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 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
(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 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 non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete 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 bool the carrier of (L ~)
bool the carrier of (L ~) is non empty set
L is set
L is Element of the carrier of L
l1 is Element of bool the carrier of L
"\/" (l1,L) is Element of the carrier of L
Y is set
Y is Element of the carrier of L
Y ~ is Element of the carrier of (L ~)
L is Relation-like Function-like set
dom L is set
L is Element of the carrier of L
waybelow L is non empty directed lower Element of bool the carrier of L
(waybelow L) /\ ((L ~)) is Element of bool the carrier of (L ~)
"\/" (((waybelow L) /\ ((L ~))),L) is Element of the carrier of L
rng L is set
{ ("\/" (b₁,L)) where b₁ is Element of bool the carrier of L : ( b₁ in rng L & "\/" (b₁,L) in waybelow L ) } is set
l1 is set
L . l1 is set
"\/" ((L . l1),L) is Element of the carrier of L
"\/" ((waybelow L),L) is Element of the carrier of L
{ b₁ where b₁ is Element of bool the carrier of L : ( b₁ in rng L & "\/" (b₁,L) in waybelow L ) } is set
union { b₁ where b₁ is Element of bool the carrier of L : ( b₁ in rng L & "\/" (b₁,L) in waybelow L ) } is set
Y is set
Y is set
x is Element of bool the carrier of L
"\/" (x,L) is Element of the carrier of L
p is Element of the carrier of L
f1 is set
L . f1 is set
{ ("\/" (b₁,L)) where b₁ is Element of bool the carrier of L : S₂[b₁] } is set
Y is set
Y is Element of bool the carrier of L
"\/" (Y,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
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 non empty set
L --> the carrier of L is non empty Relation-like non-empty non empty-yielding L -defined { the carrier of L} -valued Function-like constant V28(L) V32(L,{ the carrier of L}) Element of bool [:L,{ the carrier of L}:]
{ the carrier of L} is non empty trivial finite V44(1) set
[:L,{ the carrier of L}:] is non empty Relation-like set
bool [:L,{ the carrier of L}:] is non empty set
L is non empty Relation-like non-empty non empty-yielding L -defined Function-like V28(L) set
l1 is non empty Relation-like non-empty non empty-yielding L -defined Function-like V28(L) Function-yielding V36() ManySortedFunction of L,L --> the carrier of L
\// (l1,L) is Relation-like dom l1 -defined the carrier of L -valued Function-like V32( dom l1, the carrier of L) Element of bool [:(dom l1), the carrier of L:]
dom l1 is non empty set
[:(dom l1), the carrier of L:] is non empty Relation-like set
bool [:(dom l1), the carrier of L:] is non empty set
//\ ((\// (l1,L)),L) is Element of the carrier of L
Frege l1 is Relation-like non-empty product (doms l1) -defined Function-like V28( product (doms l1)) Function-yielding V36() ManySortedFunction of (product (doms l1)) --> L,(product (doms l1)) --> the carrier of L
doms l1 is Relation-like non-empty Function-like set
product (doms l1) is set
(product (doms l1)) --> L is Relation-like non-empty product (doms l1) -defined {L} -valued Function-like constant V28( product (doms l1)) V32( product (doms l1),{L}) Element of bool [:(product (doms l1)),{L}:]
{L} is non empty trivial finite V44(1) set
[:(product (doms l1)),{L}:] is Relation-like set
bool [:(product (doms l1)),{L}:] is non empty set
(product (doms l1)) --> the carrier of L is Relation-like non-empty product (doms l1) -defined { the carrier of L} -valued Function-like constant V28( product (doms l1)) V32( product (doms l1),{ the carrier of L}) Element of bool [:(product (doms l1)),{ the carrier of L}:]
[:(product (doms l1)),{ the carrier of L}:] is Relation-like set
bool [:(product (doms l1)),{ the carrier of L}:] is non empty set
/\\ ((Frege l1),L) is Relation-like dom (Frege l1) -defined the carrier of L -valued Function-like V32( dom (Frege l1), the carrier of L) Element of bool [:(dom (Frege l1)), the carrier of L:]
dom (Frege l1) is set
[:(dom (Frege l1)), the carrier of L:] is Relation-like set
bool [:(dom (Frege l1)), the carrier of L:] is non empty set
\\/ ((/\\ ((Frege l1),L)),L) is Element of the carrier of L
L ~ is non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete 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
waybelow (//\ ((\// (l1,L)),L)) is non empty directed lower Element of bool the carrier of L
((L ~)) is Element of bool the carrier of (L ~)
bool the carrier of (L ~) is non empty set
(waybelow (//\ ((\// (l1,L)),L))) /\ ((L ~)) is Element of bool the carrier of (L ~)
dom l1 is non empty Element of bool L
bool L is non empty set
x is Element of bool the carrier of L
p is Element of the carrier of L
p ~ is Element of the carrier of (L ~)
rng (\// (l1,L)) is non empty Element of bool the carrier of L
"/\" ((rng (\// (l1,L))),L) is Element of the carrier of L
p is Element of the carrier of L
f1 is set
L . f1 is set
l1 . f1 is Relation-like Function-like set
D is Element of L
L . D is non empty set
the Element of L . D is Element of L . D
dom (\// (l1,L)) is Element of bool (dom l1)
bool (dom l1) is non empty set
(\// (l1,L)) . D is set
l1 . D is non empty Relation-like L . D -defined the carrier of L -valued Function-like V32(L . D, the carrier of L) Element of bool [:(L . D), the carrier of L:]
[:(L . D), the carrier of L:] is non empty Relation-like set
bool [:(L . D), the carrier of L:] is non empty set
\\/ ((l1 . D),L) is Element of the carrier of L
rng (l1 . D) is non empty Element of bool the carrier of L
"\/" ((rng (l1 . D)),L) is Element of the carrier of L
P is finite Element of bool the carrier of L
"\/" (P,L) is Element of the carrier of L
(l1 . D) . the Element of L . D is Element of the carrier of L
{((l1 . D) . the Element of L . D)} is non empty trivial finite V44(1) Element of bool the carrier of L
P \/ {((l1 . D) . the Element of L . D)} is non empty finite Element of bool the carrier of L
"\/" ((P \/ {((l1 . D) . the Element of L . D)}),L) is Element of the carrier of L
R is Element of the carrier of L
dom (l1 . D) is non empty Element of bool (L . D)
bool (L . D) is non empty set
f2 is set
(l1 . D) . f2 is set
k1 is Element of L . D
(l1 . D) . k1 is Element of the carrier of L
[p,((l1 . D) . k1)] is Element of [: the carrier of L, the carrier of L:]
{p,((l1 . D) . k1)} is non empty finite set
{p} is non empty trivial finite V44(1) set
{{p,((l1 . D) . k1)},{p}} is non empty finite V41() set
[p,((l1 . D) . the Element of L . D)] is Element of [: the carrier of L, the carrier of L:]
{p,((l1 . D) . the Element of L . D)} is non empty finite set
{p} is non empty trivial finite V44(1) set
{{p,((l1 . D) . the Element of L . D)},{p}} is non empty finite V41() set
f1 is Relation-like Function-like set
dom f1 is set
D is set
dom (doms l1) is set
rng l1 is non empty V4() set
SubFuncs (rng l1) is set
l1 " (SubFuncs (rng l1)) is set
D is set
l1 . D is Relation-like Function-like set
D is set
f1 . D is set
(doms l1) . D is set
l1 . D is Relation-like Function-like set
L . D is set
[:(L . D), the carrier of L:] is Relation-like set
bool [:(L . D), the carrier of L:] is non empty set
dom (l1 . D) is set
f is Element of product (doms l1)
(Frege l1) . f is Relation-like L -defined the carrier of L -valued Function-like V32(L, the carrier of L) Element of bool [:L, the carrier of L:]
[:L, the carrier of L:] is non empty Relation-like set
bool [:L, the carrier of L:] is non empty set
rng ((Frege l1) . f) is Element of bool the carrier of L
P is Element of the carrier of L
dom ((Frege l1) . f) is Element of bool L
R is set
((Frege l1) . f) . R is set
dom (Frege l1) is Element of bool (product (doms l1))
bool (product (doms l1)) is non empty set
f2 is Element of L
((Frege l1) . f) . f2 is Element of the carrier of L
l1 . f2 is non empty Relation-like L . f2 -defined the carrier of L -valued Function-like V32(L . f2, the carrier of L) Element of bool [:(L . f2), the carrier of L:]
L . f2 is non empty set
[:(L . f2), the carrier of L:] is non empty Relation-like set
bool [:(L . f2), the carrier of L:] is non empty set
f1 . f2 is set
(l1 . f2) . (f1 . f2) is set
[p,(((Frege l1) . f) . f2)] is Element of [: the carrier of L, the carrier of L:]
{p,(((Frege l1) . f) . f2)} is non empty finite set
{p} is non empty trivial finite V44(1) set
{{p,(((Frege l1) . f) . f2)},{p}} is non empty finite V41() set
"/\" ((rng ((Frege l1) . f)),L) is Element of the carrier of L
//\ (((Frege l1) . f),L) is Element of the carrier of L
D is non empty set
D --> L is non empty Relation-like non-empty non empty-yielding D -defined {L} -valued Function-like constant V28(D) V32(D,{L}) Element of bool [:D,{L}:]
[:D,{L}:] is non empty Relation-like set
bool [:D,{L}:] is non empty set
P is non empty Relation-like D -defined Function-like V28(D) set
D --> the carrier of L is non empty Relation-like non-empty non empty-yielding D -defined { the carrier of L} -valued Function-like constant V28(D) V32(D,{ the carrier of L}) Element of bool [:D,{ the carrier of L}:]
[:D,{ the carrier of L}:] is non empty Relation-like set
bool [:D,{ the carrier of L}:] is non empty set
R is non empty Relation-like D -defined Function-like V28(D) Function-yielding V36() ManySortedFunction of P,D --> the carrier of L
f2 is Element of D
R . f2 is Relation-like P . f2 -defined the carrier of L -valued Function-like V32(P . f2, the carrier of L) Element of bool [:(P . f2), the carrier of L:]
P . f2 is set
[:(P . f2), the carrier of L:] is Relation-like set
bool [:(P . f2), the carrier of L:] is non empty set
//\ ((R . f2),L) is Element of the carrier of L
/\\ (R,L) is Relation-like dom R -defined the carrier of L -valued Function-like V32( dom R, the carrier of L) Element of bool [:(dom R), the carrier of L:]
dom R is non empty set
[:(dom R), the carrier of L:] is non empty Relation-like set
bool [:(dom R), the carrier of L:] is non empty set
rng (/\\ (R,L)) is non empty Element of bool the carrier of L
rng (/\\ ((Frege l1),L)) is Element of bool the carrier of L
"\/" ((rng (/\\ ((Frege l1),L))),L) is Element of the carrier of L
"\/" (x,L) is Element of the carrier of L
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive Heyting with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous completely-distributive RelStr
L ~ is non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive with_suprema with_infima complete RelStr
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 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 non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
L ~ is non empty strict 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 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
bool the carrier of L is non empty set
L 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
L ~ is non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive with_suprema with_infima complete RelStr
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 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 bool the carrier of (L ~)
bool the carrier of (L ~) is non empty set
bool ((L ~)) is non empty set
l1 is Element of the carrier of (L ~)
Y is Element of bool ((L ~))
"/\" (Y,(L ~)) is Element of the carrier of (L ~)
bool the carrier of L is non empty set
Y is Element of bool the carrier of L
x is Element of the carrier of L
x ~ is Element of the carrier of (L ~)
"\/" (Y,L) is Element of 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 non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive Heyting with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous completely-distributive RelStr
L ~ is non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive with_suprema with_infima complete RelStr
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 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
L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr
L ~ is non empty strict 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 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 non empty V110() reflexive transitive antisymmetric upper-bounded up-complete distributive with_suprema with_infima 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