:: WAYBEL_6 semantic presentation

REAL is set

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

{{},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

is non empty trivial functional finite V41() V44(1) set
F1() is non empty RelStr
the carrier of F1() is non empty set
bool the carrier of F1() is non empty set
F2() is Element of bool the carrier of F1()
F3() is non empty Element of bool the carrier of F1()
[:F2(),F3():] is Relation-like set
bool [:F2(),F3():] is non empty set
L is set
L is Element of F2()
L is Element of the carrier of F1()
l1 is Element of the carrier of F1()
Y is set

dom L is set
rng L is set
L is Relation-like F2() -defined F3() -valued Function-like V32(F2(),F3()) Element of bool [:F2(),F3():]
L is Element of the carrier of F1()
L . L is set
l1 is Element of F3()
Y is Element of the carrier of F1()
L is Element of the carrier of F1()
L . L is set

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:]

iter (L,l1) is Relation-like set

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

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 }:]

the carrier of L is non empty set

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

the carrier of L is non empty set

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

the carrier of L is non empty set

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

the carrier of L is non empty set

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 --> () 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 --> () 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 --> ()) .: Y is Element of bool the carrier of L
bool the carrier of L is non empty set
"\/" (((L --> ()) .: Y),L) is Element of the carrier of L
"\/" (Y,L) is Element of the carrier of L
(L --> ()) . ("\/" (Y,L)) is Element of the carrier of L
rng (L --> ()) is Element of bool the carrier of 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 --> ()) . the Element of Y is Element of the carrier of L

the carrier of L is non empty set

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

the carrier of L is non empty set

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) "/\" b1) where b1 is Element of the carrier of L : b1 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 "/\" b1) where b1 is Element of the carrier of L : b1 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 "/\" b1) where b1 is Element of the carrier of L : b1 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

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
{ b1 where b1 is Element of the carrier of L : b1 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
{ b1 where b1 is Element of the carrier of L : b1 is_way_below L } is set
Y is Element of the carrier of L

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 b1) where b1 is Element of the carrier of L : b1 in L } is set
union { (wayabove b1) where b1 is Element of the carrier of L : b1 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
{ b1 where b1 is Element of the carrier of L : Y is_way_below b1 } 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
{ b1 where b1 is Element of the carrier of L : Y is_way_below b1 } 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
{ b1 where b1 is Element of the carrier of L : Y is_way_below b1 } is set
Y is Element of 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 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

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

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 b1) where b1 is Element of the carrier of L : ex b2 being ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT st b1 = (L,l1,Y,b2) . 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

(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

(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

(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

(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

(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

(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

(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

(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

(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

(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

(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

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
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

(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 b1) where b1 is Element of the carrier of L : ex b2 being ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT st b1 = (L,l1,Y,b2) . 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
{ b1 where b1 is Element of the carrier of L : ex b2 being Element of the carrier of L st
( b2 <= b1 & b2 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

(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

(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

(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
{ b1 where b1 is Element of the carrier of L : ex b2 being Element of the carrier of L st
( b2 <= b1 & b2 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

[:(),():] is Relation-like set
bool [:(),():] is non empty set
(id ()) . 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

(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

(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

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
{ b1 where b1 is strongly_connected directed filtered Element of bool the carrier of L : ( b1 c= L ` & L in b1 ) } 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

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

f1 is set

the Element of Y is Element of Y

Y is set

"\/" (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

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

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

the carrier of L is non empty set
Top L is Element of 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 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

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
() \ {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

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

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

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
() /\ 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
() /\ L is Element of bool the carrier of 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

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
() /\ L is Element of bool the carrier of L
() /\ L is Element of bool the carrier of L
"/\" ((() /\ L),L) is Element of the carrier of L
{ ("/\" (b1,L)) where b1 is Element of bool the carrier of L : b1 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
{ b1 where b1 is Element of bool the carrier of L : ( b1 c= L & "/\" (b1,L) in Y ) } is set
union { b1 where b1 is Element of bool the carrier of L : ( b1 c= L & "/\" (b1,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
{ ("/\" (b1,L)) where b1 is Element of bool the carrier of L : S1[b1] } 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
"/\" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : S1[b1] } ,L) is Element of the carrier of L
{ b1 where b1 is Element of bool the carrier of L : S1[b1] } is set
union { b1 where b1 is Element of bool the carrier of L : S1[b1] } is set
"/\" ((union { b1 where b1 is Element of bool the carrier of L : S1[b1] } ),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

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
() /\ L is Element of bool the carrier of 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

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

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

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

Bottom L is Element of 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:]
[: 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
() ~ is Element of the carrier of (L ~)

the carrier of L is non empty set
Top L is Element of 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 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

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

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

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

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

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

the carrier of () is non empty set
[: the carrier of L, the carrier of ():] is non empty Relation-like set
bool [: the carrier of L, the carrier of ():] is non empty set
l1 is Relation-like the carrier of L -defined the carrier of () -valued Function-like V32( the carrier of L, the carrier of ()) Element of bool [: the carrier of L, the carrier of ():]
bool {L} is non empty finite V41() set

the carrier of (InclPoset ()) 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 ()
bool the carrier of () is non empty set
l1 . Y is Element of the carrier of ()
l1 . Y is Element of the carrier of ()
{(l1 . Y),(l1 . Y)} is non empty finite Element of bool the carrier of ()
Y "/\" Y is Element of the carrier of L
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of ()

l1 . (Y "/\" Y) is Element of the carrier of ()
Y "/\" Y is Element of the carrier of L
l1 . (Y "/\" Y) is Element of the carrier of ()
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of ()
{L} /\ {L} is finite set
Y "/\" Y is Element of the carrier of L
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of ()

l1 . (Y "/\" Y) is Element of the carrier of ()
Y "/\" Y is Element of the carrier of L
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of ()

l1 . (Y "/\" Y) is Element of the carrier of ()
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of ()
Y "/\" Y is Element of the carrier of L
l1 . (Y "/\" Y) is Element of the carrier of ()
(l1 . Y) "/\" (l1 . Y) is Element of the carrier of ()
Y "/\" Y is Element of the carrier of L
l1 . (Y "/\" Y) is Element of the carrier of ()
"/\" ((l1 .: {Y,Y}),()) is Element of the carrier of ()
"/\" ({Y,Y},L) is Element of the carrier of L
l1 . ("/\" ({Y,Y},L)) is Element of the carrier of ()
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 ()
bool the carrier of () is non empty set
l1 . Y is Element of the carrier of ()
l1 . Y is Element of the carrier of ()
{(l1 . Y),(l1 . Y)} is non empty finite Element of bool the carrier of ()
Y "\/" Y is Element of the carrier of L
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of ()

l1 . (Y "\/" Y) is Element of the carrier of ()
Y "\/" Y is Element of the carrier of L
l1 . (Y "\/" Y) is Element of the carrier of ()
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of ()
{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 ()
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of ()
{} \/ {L} is non empty finite set
Y "\/" Y is Element of the carrier of L
l1 . (Y "\/" Y) is Element of the carrier of ()
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of ()
{L} \/ {} is non empty finite set
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of ()
Y "\/" Y is Element of the carrier of L
l1 . (Y "\/" Y) is Element of the carrier of ()
(l1 . Y) "\/" (l1 . Y) is Element of the carrier of ()
Y "\/" Y is Element of the carrier of L
l1 . (Y "\/" Y) is Element of the carrier of ()
"\/" ((l1 .: {Y,Y}),()) is Element of the carrier of ()
"\/" ({Y,Y},L) is Element of the carrier of L
l1 . ("\/" ({Y,Y},L)) is Element of the carrier of ()
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 is non empty set
bool is non empty finite V41() set

the carrier of () 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
x is Element of the carrier of
Y is Element of the carrier of
[: the carrier of L, the carrier of :] is non empty Relation-like set
bool [: the carrier of L, the carrier of :] is non empty set
Y is Relation-like the carrier of L -defined the carrier of -valued Function-like V32( the carrier of L, the carrier of ) Element of bool [: the carrier of L, the carrier of :]
{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
bool the carrier of is non empty set
Y . L is Element of the carrier of
Y . l1 is Element of the carrier of
{(Y . L),(Y . l1)} is non empty finite Element of bool the carrier of
L "/\" l1 is Element of the carrier of L
Y . (L "/\" l1) is Element of the carrier of
"/\" ({L,l1},L) is Element of the carrier of L
Y . ("/\" ({L,l1},L)) is Element of the carrier of
"/\" ({(Y . L),(Y . l1)},) is Element of the carrier of
(Y . L) "/\" (Y . l1) is Element of the carrier of
(Y . L) /\ (Y . l1) is set

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
() ` is Element of bool the carrier of L
the carrier of L \ () is set
the carrier of 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

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 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

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

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
() ` is Element of bool the carrier of L
the carrier of 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

the carrier of 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 :] is Relation-like set
bool [: the carrier of L, the carrier of :] 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

the carrier of () 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
() ` is Element of bool the carrier of L
the carrier of L \ () is set
chi ((() `), 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 ((() `), the carrier of L)) . L is finite Element of {{},1}

the carrier of L is non empty set
[: the carrier of L, the carrier of :] is non empty Relation-like set
bool [: the carrier of L, the carrier of :] is non empty set
L is Relation-like the carrier of L -defined the carrier of -valued Function-like V32( the carrier of L, the carrier of ) Element of bool [: the carrier of L, the carrier of :]
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
() ` is Element of bool the carrier of L
the carrier of L \ () is set
chi ((() `), 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
Y is Element of the carrier of L
L . Y is Element of the carrier of

(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 ((() `), the carrier of L)) where b1 is Element of the carrier of L : b1 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