:: ROBBINS4 semantic presentation

REAL is set
NAT is non empty V24() V25() V26() Element of bool REAL
bool REAL is non empty set
NAT is non empty V24() V25() V26() set
bool NAT is non empty set
bool NAT is non empty set
2 is non empty V24() V25() V26() V30() V173() Element of NAT
[:2,2:] is V1() non empty set
[:[:2,2:],2:] is V1() non empty set
bool [:[:2,2:],2:] is non empty set
is V1() set
bool is non empty set
bool () is non empty set
K298() is non empty V180( REAL ) V183( REAL ) Element of bool ()
K317(REAL,K298()) is set
{} is V1() V2() V3() empty V24() V25() V26() V28() V29() V30() set
1 is non empty V24() V25() V26() V30() V173() Element of NAT
3 is non empty V24() V25() V26() V30() V173() Element of NAT
0 is V1() V2() V3() empty V24() V25() V26() V28() V29() V30() Element of NAT
K165(NAT,0,1,2) is non empty Element of bool NAT
3 \ 1 is Element of bool 3
bool 3 is non empty set
K164(NAT,1,2) is non empty Element of bool NAT
3 \ 2 is Element of bool 3
K163(NAT,2) is non empty Element of bool NAT
is non empty set
{{},1} is non empty set
{{},1,2} is non empty set

the carrier of L is non empty set
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

the carrier of L is non empty set
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

the carrier of L9 is non empty set
the L_join of L9 is V1() Function-like V18([: the carrier of L9, the carrier of L9:], the carrier of L9) Element of bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:]
[: the carrier of L9, the carrier of L9:] is V1() non empty set
[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is V1() non empty set
bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is non empty set
the L_meet of L9 is V1() Function-like V18([: the carrier of L9, the carrier of L9:], the carrier of L9) Element of bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:]

LattRel L is V1() V14( the carrier of L) V157() V160() V164() Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L,() #) is strict RelStr

LattRel L9 is V1() V14( the carrier of L9) V157() V160() V164() Element of bool [: the carrier of L9, the carrier of L9:]
bool [: the carrier of L9, the carrier of L9:] is non empty set
RelStr(# the carrier of L9,(LattRel L9) #) is strict RelStr
LattRel L is V1() V14( the carrier of L) V157() V160() V164() Element of bool [: the carrier of L, the carrier of L:]
LattRel L9 is V1() V14( the carrier of L9) V157() V160() V164() Element of bool [: the carrier of L9, the carrier of L9:]
L9 is Element of the carrier of L
c is Element of the carrier of L
[L9,c] is set
{L9,c} is non empty set
{L9} is non empty set
{{L9,c},{L9}} is non empty set
L9 "\/" c is Element of the carrier of L
the L_join of L . (L9,c) is Element of the carrier of L
v2 is Element of the carrier of L9
v1 is Element of the carrier of L9
v2 "\/" v1 is Element of the carrier of L9
the L_join of L9 . (v2,v1) is Element of the carrier of L9

the carrier of L is non empty set
the Element of the carrier of L is Element of the carrier of L
the Element of the carrier of L ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . the Element of the carrier of L is Element of the carrier of L
( the Element of the carrier of L `) ` is Element of the carrier of L
the Compl of L . ( the Element of the carrier of L `) is Element of the carrier of L
(( the Element of the carrier of L `) `) "\/" ( the Element of the carrier of L `) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . ((( the Element of the carrier of L `) `),( the Element of the carrier of L `)) is Element of the carrier of L
((( the Element of the carrier of L `) `) "\/" ( the Element of the carrier of L `)) ` is Element of the carrier of L
the Compl of L . ((( the Element of the carrier of L `) `) "\/" ( the Element of the carrier of L `)) is Element of the carrier of L
L9 is Element of the carrier of L
c is Element of the carrier of L
L9 "/\" c is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . (L9,c) is Element of the carrier of L
c "/\" L9 is Element of the carrier of L
the L_meet of L . (c,L9) is Element of the carrier of L
c ` is Element of the carrier of L
the Compl of L . c is Element of the carrier of L
(c `) ` is Element of the carrier of L
the Compl of L . (c `) is Element of the carrier of L
((c `) `) "\/" (c `) is Element of the carrier of L
the L_join of L . (((c `) `),(c `)) is Element of the carrier of L
(((c `) `) "\/" (c `)) ` is Element of the carrier of L
the Compl of L . (((c `) `) "\/" (c `)) is Element of the carrier of L
((((c `) `) "\/" (c `)) `) "/\" c is Element of the carrier of L
the L_meet of L . (((((c `) `) "\/" (c `)) `),c) is Element of the carrier of L
(c `) "/\" c is Element of the carrier of L
the L_meet of L . ((c `),c) is Element of the carrier of L
((c `) "/\" c) "/\" c is Element of the carrier of L
the L_meet of L . (((c `) "/\" c),c) is Element of the carrier of L
c "/\" c is Element of the carrier of L
the L_meet of L . (c,c) is Element of the carrier of L
(c `) "/\" (c "/\" c) is Element of the carrier of L
the L_meet of L . ((c `),(c "/\" c)) is Element of the carrier of L
L9 is Element of the carrier of L

the carrier of L is non empty set
the Element of the carrier of L is Element of the carrier of L
the Element of the carrier of L ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . the Element of the carrier of L is Element of the carrier of L
( the Element of the carrier of L `) "\/" the Element of the carrier of L is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (( the Element of the carrier of L `), the Element of the carrier of L) is Element of the carrier of L
L9 is Element of the carrier of L
c is Element of the carrier of L
L9 "\/" c is Element of the carrier of L
the L_join of L . (L9,c) is Element of the carrier of L
c "\/" L9 is Element of the carrier of L
the L_join of L . (c,L9) is Element of the carrier of L
c ` is Element of the carrier of L
the Compl of L . c is Element of the carrier of L
(c `) "\/" c is Element of the carrier of L
the L_join of L . ((c `),c) is Element of the carrier of L
((c `) "\/" c) "\/" c is Element of the carrier of L
the L_join of L . (((c `) "\/" c),c) is Element of the carrier of L
c "\/" c is Element of the carrier of L
the L_join of L . (c,c) is Element of the carrier of L
(c `) "\/" (c "\/" c) is Element of the carrier of L
the L_join of L . ((c `),(c "\/" c)) is Element of the carrier of L
L9 is Element of the carrier of L

the carrier of L is non empty set
Top L is Element of the carrier of L
Bottom L is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 "\/" (L9 `) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (L9,(L9 `)) is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
L9 is Element of the carrier of L
(L9 "\/" (L9 `)) "\/" L9 is Element of the carrier of L
the L_join of L . ((L9 "\/" (L9 `)),L9) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
L9 "\/" (L9 `) is Element of the carrier of L
the L_join of L . (L9,(L9 `)) is Element of the carrier of L
(L9 "\/" (L9 `)) "\/" L9 is Element of the carrier of L
the L_join of L . ((L9 "\/" (L9 `)),L9) is Element of the carrier of L
L9 "\/" L9 is Element of the carrier of L
the L_join of L . (L9,L9) is Element of the carrier of L
(L9 `) "\/" (L9 "\/" L9) is Element of the carrier of L
the L_join of L . ((L9 `),(L9 "\/" L9)) is Element of the carrier of L
(L9 `) "\/" L9 is Element of the carrier of L
the L_join of L . ((L9 `),L9) is Element of the carrier of L
L9 is Element of the carrier of L
L9 "\/" (L9 "\/" (L9 `)) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" (L9 `))) is Element of the carrier of L
L9 is Element of the carrier of L
(L9 "/\" (L9 `)) "/\" L9 is Element of the carrier of L
the L_meet of L . ((L9 "/\" (L9 `)),L9) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
(L9 `) "\/" ((L9 `) `) is Element of the carrier of L
the L_join of L . ((L9 `),((L9 `) `)) is Element of the carrier of L
((L9 `) "\/" ((L9 `) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" ((L9 `) `)) is Element of the carrier of L
(((L9 `) "\/" ((L9 `) `)) `) "/\" L9 is Element of the carrier of L
the L_meet of L . ((((L9 `) "\/" ((L9 `) `)) `),L9) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
(L9 `) "\/" ((L9 `) `) is Element of the carrier of L
the L_join of L . ((L9 `),((L9 `) `)) is Element of the carrier of L
((L9 `) "\/" ((L9 `) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" ((L9 `) `)) is Element of the carrier of L
(((L9 `) "\/" ((L9 `) `)) `) "/\" L9 is Element of the carrier of L
the L_meet of L . ((((L9 `) "\/" ((L9 `) `)) `),L9) is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
(L9 "/\" (L9 `)) "/\" L9 is Element of the carrier of L
the L_meet of L . ((L9 "/\" (L9 `)),L9) is Element of the carrier of L
L9 "/\" L9 is Element of the carrier of L
the L_meet of L . (L9,L9) is Element of the carrier of L
(L9 `) "/\" (L9 "/\" L9) is Element of the carrier of L
the L_meet of L . ((L9 `),(L9 "/\" L9)) is Element of the carrier of L
(L9 `) "/\" L9 is Element of the carrier of L
the L_meet of L . ((L9 `),L9) is Element of the carrier of L
((L9 `) `) "\/" (L9 `) is Element of the carrier of L
the L_join of L . (((L9 `) `),(L9 `)) is Element of the carrier of L
(((L9 `) `) "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . (((L9 `) `) "\/" (L9 `)) is Element of the carrier of L
((L9 `) `) "\/" (L9 `) is Element of the carrier of L
the L_join of L . (((L9 `) `),(L9 `)) is Element of the carrier of L
(((L9 `) `) "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . (((L9 `) `) "\/" (L9 `)) is Element of the carrier of L
L9 is Element of the carrier of L
L9 "/\" (L9 "/\" (L9 `)) is Element of the carrier of L
the L_meet of L . (L9,(L9 "/\" (L9 `))) is Element of the carrier of L
L is non empty OrthoLattStr
the carrier of L is non empty set
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 "\/" L9 is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (L9,L9) is Element of the carrier of L
c is Element of the carrier of L
(L9 "\/" L9) "\/" c is Element of the carrier of L
the L_join of L . ((L9 "\/" L9),c) is Element of the carrier of L
c ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . c is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
(c `) "/\" (L9 `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . ((c `),(L9 `)) is Element of the carrier of L
((c `) "/\" (L9 `)) ` is Element of the carrier of L
the Compl of L . ((c `) "/\" (L9 `)) is Element of the carrier of L
(((c `) "/\" (L9 `)) `) "\/" L9 is Element of the carrier of L
the L_join of L . ((((c `) "/\" (L9 `)) `),L9) is Element of the carrier of L
(c `) ` is Element of the carrier of L
the Compl of L . (c `) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
((c `) `) "\/" ((L9 `) `) is Element of the carrier of L
the L_join of L . (((c `) `),((L9 `) `)) is Element of the carrier of L
(((c `) `) "\/" ((L9 `) `)) ` is Element of the carrier of L
the Compl of L . (((c `) `) "\/" ((L9 `) `)) is Element of the carrier of L
((((c `) `) "\/" ((L9 `) `)) `) ` is Element of the carrier of L
the Compl of L . ((((c `) `) "\/" ((L9 `) `)) `) is Element of the carrier of L
(((((c `) `) "\/" ((L9 `) `)) `) `) "\/" L9 is Element of the carrier of L
the L_join of L . ((((((c `) `) "\/" ((L9 `) `)) `) `),L9) is Element of the carrier of L
c "\/" ((L9 `) `) is Element of the carrier of L
the L_join of L . (c,((L9 `) `)) is Element of the carrier of L
(c "\/" ((L9 `) `)) ` is Element of the carrier of L
the Compl of L . (c "\/" ((L9 `) `)) is Element of the carrier of L
((c "\/" ((L9 `) `)) `) ` is Element of the carrier of L
the Compl of L . ((c "\/" ((L9 `) `)) `) is Element of the carrier of L
(((c "\/" ((L9 `) `)) `) `) "\/" L9 is Element of the carrier of L
the L_join of L . ((((c "\/" ((L9 `) `)) `) `),L9) is Element of the carrier of L
c "\/" L9 is Element of the carrier of L
the L_join of L . (c,L9) is Element of the carrier of L
(c "\/" L9) ` is Element of the carrier of L
the Compl of L . (c "\/" L9) is Element of the carrier of L
((c "\/" L9) `) ` is Element of the carrier of L
the Compl of L . ((c "\/" L9) `) is Element of the carrier of L
(((c "\/" L9) `) `) "\/" L9 is Element of the carrier of L
the L_join of L . ((((c "\/" L9) `) `),L9) is Element of the carrier of L
(c "\/" L9) "\/" L9 is Element of the carrier of L
the L_join of L . ((c "\/" L9),L9) is Element of the carrier of L
L9 "\/" (c "\/" L9) is Element of the carrier of L
the L_join of L . (L9,(c "\/" L9)) is Element of the carrier of L
c "\/" (L9 "\/" L9) is Element of the carrier of L
the L_join of L . (c,(L9 "\/" L9)) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 "\/" L9 is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (L9,L9) is Element of the carrier of L
L9 "/\" (L9 "\/" L9) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . (L9,(L9 "\/" L9)) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
L9 "\/" (L9 "/\" (L9 `)) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . (L9,(L9 "/\" (L9 `))) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
(L9 `) "\/" ((L9 `) `) is Element of the carrier of L
the L_join of L . ((L9 `),((L9 `) `)) is Element of the carrier of L
((L9 `) "\/" ((L9 `) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" ((L9 `) `)) is Element of the carrier of L
L9 "\/" (((L9 `) "\/" ((L9 `) `)) `) is Element of the carrier of L
the L_join of L . (L9,(((L9 `) "\/" ((L9 `) `)) `)) is Element of the carrier of L
(L9 `) "\/" L9 is Element of the carrier of L
the L_join of L . ((L9 `),L9) is Element of the carrier of L
((L9 `) "\/" L9) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" L9) is Element of the carrier of L
L9 "\/" (((L9 `) "\/" L9) `) is Element of the carrier of L
the L_join of L . (L9,(((L9 `) "\/" L9) `)) is Element of the carrier of L
L9 "\/" (L9 `) is Element of the carrier of L
the L_join of L . (L9,(L9 `)) is Element of the carrier of L
(L9 "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . (L9 "\/" (L9 `)) is Element of the carrier of L
L9 "\/" ((L9 "\/" (L9 `)) `) is Element of the carrier of L
the L_join of L . (L9,((L9 "\/" (L9 `)) `)) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
L9 "\/" (L9 `) is Element of the carrier of L
the L_join of L . (L9,(L9 `)) is Element of the carrier of L
(L9 "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . (L9 "\/" (L9 `)) is Element of the carrier of L
L9 "\/" ((L9 "\/" (L9 `)) `) is Element of the carrier of L
the L_join of L . (L9,((L9 "\/" (L9 `)) `)) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
((L9 `) `) "\/" (L9 `) is Element of the carrier of L
the L_join of L . (((L9 `) `),(L9 `)) is Element of the carrier of L
(((L9 `) `) "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . (((L9 `) `) "\/" (L9 `)) is Element of the carrier of L
L9 "\/" ((((L9 `) `) "\/" (L9 `)) `) is Element of the carrier of L
the L_join of L . (L9,((((L9 `) `) "\/" (L9 `)) `)) is Element of the carrier of L
(L9 `) "/\" L9 is Element of the carrier of L
the L_meet of L . ((L9 `),L9) is Element of the carrier of L
L9 "\/" ((L9 `) "/\" L9) is Element of the carrier of L
the L_join of L . (L9,((L9 `) "/\" L9)) is Element of the carrier of L
((L9 `) "/\" L9) "\/" L9 is Element of the carrier of L
the L_join of L . (((L9 `) "/\" L9),L9) is Element of the carrier of L
L9 is Element of the carrier of L
L9 "/\" L9 is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,L9) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
L9 "\/" (L9 "/\" (L9 `)) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . (L9,(L9 "/\" (L9 `))) is Element of the carrier of L
L9 "/\" (L9 "\/" (L9 "/\" (L9 `))) is Element of the carrier of L
the L_meet of L . (L9,(L9 "\/" (L9 "/\" (L9 `)))) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
(L9 "/\" (L9 `)) ` is Element of the carrier of L
the Compl of L . (L9 "/\" (L9 `)) is Element of the carrier of L
((L9 "/\" (L9 `)) `) ` is Element of the carrier of L
the Compl of L . ((L9 "/\" (L9 `)) `) is Element of the carrier of L
(((L9 "/\" (L9 `)) `) `) "\/" L9 is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . ((((L9 "/\" (L9 `)) `) `),L9) is Element of the carrier of L
L9 "\/" (L9 "/\" (L9 `)) is Element of the carrier of L
the L_join of L . (L9,(L9 "/\" (L9 `))) is Element of the carrier of L
(L9 "\/" (L9 "/\" (L9 `))) "\/" (L9 "/\" (L9 `)) is Element of the carrier of L
the L_join of L . ((L9 "\/" (L9 "/\" (L9 `))),(L9 "/\" (L9 `))) is Element of the carrier of L
((L9 "/\" (L9 `)) `) "/\" ((L9 "/\" (L9 `)) `) is Element of the carrier of L
the L_meet of L . (((L9 "/\" (L9 `)) `),((L9 "/\" (L9 `)) `)) is Element of the carrier of L
(((L9 "/\" (L9 `)) `) "/\" ((L9 "/\" (L9 `)) `)) ` is Element of the carrier of L
the Compl of L . (((L9 "/\" (L9 `)) `) "/\" ((L9 "/\" (L9 `)) `)) is Element of the carrier of L
((((L9 "/\" (L9 `)) `) "/\" ((L9 "/\" (L9 `)) `)) `) "\/" L9 is Element of the carrier of L
the L_join of L . (((((L9 "/\" (L9 `)) `) "/\" ((L9 "/\" (L9 `)) `)) `),L9) is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
(L9 "/\" (L9 `)) ` is Element of the carrier of L
the Compl of L . (L9 "/\" (L9 `)) is Element of the carrier of L
((L9 "/\" (L9 `)) `) ` is Element of the carrier of L
the Compl of L . ((L9 "/\" (L9 `)) `) is Element of the carrier of L
(((L9 "/\" (L9 `)) `) `) "\/" (L9 "/\" (L9 `)) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . ((((L9 "/\" (L9 `)) `) `),(L9 "/\" (L9 `))) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
(L9 "/\" (L9 `)) "\/" L9 is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . ((L9 "/\" (L9 `)),L9) is Element of the carrier of L
(L9 "/\" (L9 `)) ` is Element of the carrier of L
the Compl of L . (L9 "/\" (L9 `)) is Element of the carrier of L
((L9 "/\" (L9 `)) `) ` is Element of the carrier of L
the Compl of L . ((L9 "/\" (L9 `)) `) is Element of the carrier of L
(((L9 "/\" (L9 `)) `) `) "\/" L9 is Element of the carrier of L
the L_join of L . ((((L9 "/\" (L9 `)) `) `),L9) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 "\/" L9 is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (L9,L9) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
(L9 `) "/\" (L9 `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . ((L9 `),(L9 `)) is Element of the carrier of L
((L9 `) "/\" (L9 `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "/\" (L9 `)) is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
(L9 "/\" (L9 `)) "\/" L9 is Element of the carrier of L
the L_join of L . ((L9 "/\" (L9 `)),L9) is Element of the carrier of L
((L9 "/\" (L9 `)) "\/" L9) "\/" L9 is Element of the carrier of L
the L_join of L . (((L9 "/\" (L9 `)) "\/" L9),L9) is Element of the carrier of L
(((L9 `) "/\" (L9 `)) `) "\/" (L9 "/\" (L9 `)) is Element of the carrier of L
the L_join of L . ((((L9 `) "/\" (L9 `)) `),(L9 "/\" (L9 `))) is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
(L9 `) "\/" L9 is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . ((L9 `),L9) is Element of the carrier of L
(L9 `) "/\" ((L9 `) "\/" L9) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . ((L9 `),((L9 `) "\/" L9)) is Element of the carrier of L
(L9 `) "/\" ((L9 `) `) is Element of the carrier of L
the L_meet of L . ((L9 `),((L9 `) `)) is Element of the carrier of L
((L9 `) "/\" ((L9 `) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "/\" ((L9 `) `)) is Element of the carrier of L
((L9 `) "/\" ((L9 `) `)) "\/" L9 is Element of the carrier of L
the L_join of L . (((L9 `) "/\" ((L9 `) `)),L9) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 "\/" L9 is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (L9,L9) is Element of the carrier of L
L9 "\/" L9 is Element of the carrier of L
the L_join of L . (L9,L9) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
(L9 "/\" (L9 `)) "\/" L9 is Element of the carrier of L
the L_join of L . ((L9 "/\" (L9 `)),L9) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
(L9 "/\" (L9 `)) ` is Element of the carrier of L
the Compl of L . (L9 "/\" (L9 `)) is Element of the carrier of L
(L9 `) "/\" ((L9 "/\" (L9 `)) `) is Element of the carrier of L
the L_meet of L . ((L9 `),((L9 "/\" (L9 `)) `)) is Element of the carrier of L
((L9 `) "/\" ((L9 "/\" (L9 `)) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "/\" ((L9 "/\" (L9 `)) `)) is Element of the carrier of L
(((L9 `) "/\" ((L9 "/\" (L9 `)) `)) `) "\/" L9 is Element of the carrier of L
the L_join of L . ((((L9 `) "/\" ((L9 "/\" (L9 `)) `)) `),L9) is Element of the carrier of L
L9 "\/" (L9 "/\" (L9 `)) is Element of the carrier of L
the L_join of L . (L9,(L9 "/\" (L9 `))) is Element of the carrier of L
(L9 "\/" (L9 "/\" (L9 `))) "\/" L9 is Element of the carrier of L
the L_join of L . ((L9 "\/" (L9 "/\" (L9 `))),L9) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 "/\" L9 is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,L9) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
(L9 `) "\/" (L9 `) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . ((L9 `),(L9 `)) is Element of the carrier of L
((L9 `) "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" (L9 `)) is Element of the carrier of L
(L9 `) "\/" (L9 `) is Element of the carrier of L
the L_join of L . ((L9 `),(L9 `)) is Element of the carrier of L
((L9 `) "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" (L9 `)) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
((L9 `) `) "/\" ((L9 `) `) is Element of the carrier of L
the L_meet of L . (((L9 `) `),((L9 `) `)) is Element of the carrier of L
(((L9 `) `) "/\" ((L9 `) `)) ` is Element of the carrier of L
the Compl of L . (((L9 `) `) "/\" ((L9 `) `)) is Element of the carrier of L
((((L9 `) `) "/\" ((L9 `) `)) `) ` is Element of the carrier of L
the Compl of L . ((((L9 `) `) "/\" ((L9 `) `)) `) is Element of the carrier of L
((L9 `) `) "/\" L9 is Element of the carrier of L
the L_meet of L . (((L9 `) `),L9) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 "/\" L9 is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,L9) is Element of the carrier of L
(L9 "/\" L9) "\/" L9 is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . ((L9 "/\" L9),L9) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
(L9 "/\" L9) ` is Element of the carrier of L
the Compl of L . (L9 "/\" L9) is Element of the carrier of L
(L9 `) "/\" ((L9 "/\" L9) `) is Element of the carrier of L
the L_meet of L . ((L9 `),((L9 "/\" L9) `)) is Element of the carrier of L
((L9 `) "/\" ((L9 "/\" L9) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "/\" ((L9 "/\" L9) `)) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
(L9 `) "\/" (L9 `) is Element of the carrier of L
the L_join of L . ((L9 `),(L9 `)) is Element of the carrier of L
((L9 `) "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" (L9 `)) is Element of the carrier of L
(((L9 `) "\/" (L9 `)) `) ` is Element of the carrier of L
the Compl of L . (((L9 `) "\/" (L9 `)) `) is Element of the carrier of L
(L9 `) "/\" ((((L9 `) "\/" (L9 `)) `) `) is Element of the carrier of L
the L_meet of L . ((L9 `),((((L9 `) "\/" (L9 `)) `) `)) is Element of the carrier of L
((L9 `) "/\" ((((L9 `) "\/" (L9 `)) `) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "/\" ((((L9 `) "\/" (L9 `)) `) `)) is Element of the carrier of L
(L9 `) "/\" ((L9 `) "\/" (L9 `)) is Element of the carrier of L
the L_meet of L . ((L9 `),((L9 `) "\/" (L9 `))) is Element of the carrier of L
((L9 `) "/\" ((L9 `) "\/" (L9 `))) ` is Element of the carrier of L
the Compl of L . ((L9 `) "/\" ((L9 `) "\/" (L9 `))) is Element of the carrier of L
(L9 `) "\/" (L9 `) is Element of the carrier of L
the L_join of L . ((L9 `),(L9 `)) is Element of the carrier of L
(L9 `) "/\" ((L9 `) "\/" (L9 `)) is Element of the carrier of L
the L_meet of L . ((L9 `),((L9 `) "\/" (L9 `))) is Element of the carrier of L
((L9 `) "/\" ((L9 `) "\/" (L9 `))) ` is Element of the carrier of L
the Compl of L . ((L9 `) "/\" ((L9 `) "\/" (L9 `))) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
c is Element of the carrier of L
L9 "\/" c is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (L9,c) is Element of the carrier of L
L9 "\/" (L9 "\/" c) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" c)) is Element of the carrier of L
L9 "\/" L9 is Element of the carrier of L
the L_join of L . (L9,L9) is Element of the carrier of L
(L9 "\/" L9) "\/" c is Element of the carrier of L
the L_join of L . ((L9 "\/" L9),c) is Element of the carrier of L
c ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . c is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
(c `) "/\" (L9 `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . ((c `),(L9 `)) is Element of the carrier of L
((c `) "/\" (L9 `)) ` is Element of the carrier of L
the Compl of L . ((c `) "/\" (L9 `)) is Element of the carrier of L
(((c `) "/\" (L9 `)) `) "\/" L9 is Element of the carrier of L
the L_join of L . ((((c `) "/\" (L9 `)) `),L9) is Element of the carrier of L
(L9 "\/" c) "\/" L9 is Element of the carrier of L
the L_join of L . ((L9 "\/" c),L9) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
c is Element of the carrier of L
L9 "/\" c is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,c) is Element of the carrier of L
L9 "/\" (L9 "/\" c) is Element of the carrier of L
the L_meet of L . (L9,(L9 "/\" c)) is Element of the carrier of L
L9 "/\" L9 is Element of the carrier of L
the L_meet of L . (L9,L9) is Element of the carrier of L
(L9 "/\" L9) "/\" c is Element of the carrier of L
the L_meet of L . ((L9 "/\" L9),c) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
(L9 "/\" c) ` is Element of the carrier of L
the Compl of L . (L9 "/\" c) is Element of the carrier of L
(L9 `) "\/" ((L9 "/\" c) `) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . ((L9 `),((L9 "/\" c) `)) is Element of the carrier of L
((L9 `) "\/" ((L9 "/\" c) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" ((L9 "/\" c) `)) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
c ` is Element of the carrier of L
the Compl of L . c is Element of the carrier of L
(L9 `) "\/" (c `) is Element of the carrier of L
the L_join of L . ((L9 `),(c `)) is Element of the carrier of L
((L9 `) "\/" (c `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" (c `)) is Element of the carrier of L
(((L9 `) "\/" (c `)) `) ` is Element of the carrier of L
the Compl of L . (((L9 `) "\/" (c `)) `) is Element of the carrier of L
(L9 `) "\/" ((((L9 `) "\/" (c `)) `) `) is Element of the carrier of L
the L_join of L . ((L9 `),((((L9 `) "\/" (c `)) `) `)) is Element of the carrier of L
((L9 `) "\/" ((((L9 `) "\/" (c `)) `) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" ((((L9 `) "\/" (c `)) `) `)) is Element of the carrier of L
(L9 `) "\/" ((L9 `) "\/" (c `)) is Element of the carrier of L
the L_join of L . ((L9 `),((L9 `) "\/" (c `))) is Element of the carrier of L
((L9 `) "\/" ((L9 `) "\/" (c `))) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" ((L9 `) "\/" (c `))) is Element of the carrier of L
(L9 `) "\/" (L9 `) is Element of the carrier of L
the L_join of L . ((L9 `),(L9 `)) is Element of the carrier of L
((L9 `) "\/" (L9 `)) "\/" (c `) is Element of the carrier of L
the L_join of L . (((L9 `) "\/" (L9 `)),(c `)) is Element of the carrier of L
(((L9 `) "\/" (L9 `)) "\/" (c `)) ` is Element of the carrier of L
the Compl of L . (((L9 `) "\/" (L9 `)) "\/" (c `)) is Element of the carrier of L
((L9 `) "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" (L9 `)) is Element of the carrier of L
(((L9 `) "\/" (L9 `)) `) ` is Element of the carrier of L
the Compl of L . (((L9 `) "\/" (L9 `)) `) is Element of the carrier of L
((((L9 `) "\/" (L9 `)) `) `) "\/" (c `) is Element of the carrier of L
the L_join of L . (((((L9 `) "\/" (L9 `)) `) `),(c `)) is Element of the carrier of L
(((((L9 `) "\/" (L9 `)) `) `) "\/" (c `)) ` is Element of the carrier of L
the Compl of L . (((((L9 `) "\/" (L9 `)) `) `) "\/" (c `)) is Element of the carrier of L
(L9 "/\" L9) ` is Element of the carrier of L
the Compl of L . (L9 "/\" L9) is Element of the carrier of L
((L9 "/\" L9) `) "\/" (c `) is Element of the carrier of L
the L_join of L . (((L9 "/\" L9) `),(c `)) is Element of the carrier of L
(((L9 "/\" L9) `) "\/" (c `)) ` is Element of the carrier of L
the Compl of L . (((L9 "/\" L9) `) "\/" (c `)) is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
L9 "/\" (L9 `) is Element of the carrier of L
the L_meet of L . (L9,(L9 `)) is Element of the carrier of L
(L9 "/\" (L9 `)) "\/" (L9 "/\" (L9 `)) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . ((L9 "/\" (L9 `)),(L9 "/\" (L9 `))) is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 "\/" (L9 `) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (L9,(L9 `)) is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
L9 "\/" (L9 `) is Element of the carrier of L
the L_join of L . (L9,(L9 `)) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
(L9 `) "/\" ((L9 `) `) is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . ((L9 `),((L9 `) `)) is Element of the carrier of L
((L9 `) "/\" ((L9 `) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "/\" ((L9 `) `)) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
(L9 `) "/\" ((L9 `) `) is Element of the carrier of L
the L_meet of L . ((L9 `),((L9 `) `)) is Element of the carrier of L
((L9 `) "/\" ((L9 `) `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "/\" ((L9 `) `)) is Element of the carrier of L
(L9 `) "\/" L9 is Element of the carrier of L
the L_join of L . ((L9 `),L9) is Element of the carrier of L
(L9 `) "\/" L9 is Element of the carrier of L
the L_join of L . ((L9 `),L9) is Element of the carrier of L

the carrier of L is non empty set
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
L9 "/\" L9 is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,L9) is Element of the carrier of L
(L9 "/\" L9) ` is Element of the carrier of L
the Compl of L . (L9 "/\" L9) is Element of the carrier of L
(L9 `) "\/" (L9 `) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . ((L9 `),(L9 `)) is Element of the carrier of L
((L9 `) "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" (L9 `)) is Element of the carrier of L
(((L9 `) "\/" (L9 `)) `) ` is Element of the carrier of L
the Compl of L . (((L9 `) "\/" (L9 `)) `) is Element of the carrier of L
(L9 `) "\/" (L9 `) is Element of the carrier of L
the L_join of L . ((L9 `),(L9 `)) is Element of the carrier of L
(L9 `) "/\" (L9 `) is Element of the carrier of L
the L_meet of L . ((L9 `),(L9 `)) is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 "/\" L9 is Element of the carrier of L
the L_meet of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is V1() non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L9,L9) is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L is V1() Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
the Compl of L . L9 is Element of the carrier of L
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
(L9 `) "\/" (L9 `) is Element of the carrier of L
the L_join of L is V1() Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_join of L . ((L9 `),(L9 `)) is Element of the carrier of L
((L9 `) "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" (L9 `)) is Element of the carrier of L
(L9 `) "\/" (L9 `) is Element of the carrier of L
((L9 `) "\/" (L9 `)) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" (L9 `)) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
L9 "/\" L9 is Element of the carrier of L
(L9 "/\" L9) ` is Element of the carrier of L
the Compl of L . (L9 "/\" L9) is Element of the carrier of L
((L9 "/\" L9) `) ` is Element of the carrier of L
the Compl of L . ((L9 "/\" L9) `) is Element of the carrier of L
(L9 `) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L

[::] is V1() non empty set
bool [::] is non empty set

[::] is V1() non empty set
bool [::] is non empty set