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
[:NAT,REAL:] is V1() set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
K298() is non empty V180( REAL ) V183( REAL ) Element of bool (bool REAL)
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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing 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:]
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing 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:]
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing LattStr
L9 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing LattStr
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:]
LattStr(# the carrier of L9, the L_join of L9, the L_meet of L9 #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing LattStr
LattPOSet L is strict reflexive transitive antisymmetric with_suprema with_infima RelStr
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,(LattRel L) #) is strict RelStr
LattPOSet L9 is strict reflexive transitive antisymmetric with_suprema with_infima 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
L is non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing involutive 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 ` 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
the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr is non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr is non empty trivial V32() set
L9 is Element of the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
L9 is Element of the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
L9 ` is Element of the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the Compl of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr is V1() Function-like V18( the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr , the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr ) Element of bool [: the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr , the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :]
[: the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr , the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :] is V1() non empty set
bool [: the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr , the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :] is non empty set
the Compl of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr . L9 is Element of the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
(L9 `) "/\" L9 is Element of the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the L_meet of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr is V1() Function-like V18([: the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr , the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :], the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr ) Element of bool [:[: the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr , the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :], the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :]
[:[: the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr , the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :], the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :] is V1() non empty set
bool [:[: the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr , the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :], the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :] is non empty set
the L_meet of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr . ((L9 `),L9) is Element of the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
L9 "\/" ((L9 `) "/\" L9) is Element of the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the L_join of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr is V1() Function-like V18([: the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr , the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :], the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr ) Element of bool [:[: the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr , the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :], the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr :]
the L_join of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr . (L9,((L9 `) "/\" L9)) is Element of the carrier of the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like modular lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top 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 ` 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
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_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 `)) "/\" 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 join-associative meet-commutative meet-absorbing join-absorbing () 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
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
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 `) "/\" (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
L is non empty join-associative meet-commutative meet-absorbing join-absorbing 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 ` 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 L_join of L . (L9,L9) is Element of the carrier of L
L is non empty join-associative meet-commutative meet-absorbing join-absorbing 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
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
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 `) "/\" (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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top () () OrthoLattStr is non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top () () OrthoLattStr
{0,1,(3 \ 1),2,(3 \ 2),3} is non empty set
InclPoset {0,1,(3 \ 1),2,(3 \ 2),3} is non empty strict reflexive transitive antisymmetric RelStr
() is RelStr
the carrier of () is non empty set
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
1 \/ (3 \ 1) is non empty set
1 \/ 3 is non empty set
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
1 \/ (3 \ 1) is non empty set
1 \/ 3 is non empty set
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
2 \/ (3 \ 2) is non empty set
2 \/ 3 is non empty set
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
2 \/ (3 \ 2) is non empty set
2 \/ 3 is non empty set
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 \/ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
(3 \ 1) /\ 3 is Element of bool 3
3 /\ 3 is set
(3 /\ 3) \ 1 is Element of bool (3 /\ 3)
bool (3 /\ 3) is non empty set
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
2 /\ (3 \ 2) is Element of bool 3
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
2 /\ (3 \ 2) is Element of bool 3
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
(3 \ 2) /\ 3 is Element of bool 3
3 /\ 3 is set
(3 /\ 3) \ 2 is Element of bool (3 /\ 3)
bool (3 /\ 3) is non empty set
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
(3 \ 1) /\ 3 is Element of bool 3
3 /\ 3 is set
(3 /\ 3) \ 1 is Element of bool (3 /\ 3)
bool (3 /\ 3) is non empty set
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
(3 \ 2) /\ 3 is Element of bool 3
3 /\ 3 is set
(3 /\ 3) \ 2 is Element of bool (3 /\ 3)
bool (3 /\ 3) is non empty set
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
L9 /\ c is set
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
latt () is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing LattStr
the carrier of (latt ()) is non empty set
the carrier of () is non empty set
the InternalRel of () is V1() Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is V1() non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (), the InternalRel of () #) is strict RelStr
LattPOSet (latt ()) is strict reflexive transitive antisymmetric with_suprema with_infima RelStr
LattRel (latt ()) is V1() V14( the carrier of (latt ())) V157() V160() V164() Element of bool [: the carrier of (latt ()), the carrier of (latt ()):]
[: the carrier of (latt ()), the carrier of (latt ()):] is V1() non empty set
bool [: the carrier of (latt ()), the carrier of (latt ()):] is non empty set
RelStr(# the carrier of (latt ()),(LattRel (latt ())) #) is strict RelStr
L is set
the L_join of (latt ()) is V1() Function-like V18([: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ())) Element of bool [:[: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ()):]
[: the carrier of (latt ()), the carrier of (latt ()):] is V1() non empty set
[:[: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ()):] is V1() non empty set
bool [:[: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ()):] is non empty set
the L_meet of (latt ()) is V1() Function-like V18([: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ())) Element of bool [:[: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ()):]
v2 is Element of the carrier of (latt ())
v1 is Element of bool 3
v1 ` is Element of bool 3
3 \ v1 is set
v1 is Element of bool 3
v1 ` is Element of bool 3
3 \ v1 is set
v1 is Element of bool 3
v1 ` is Element of bool 3
3 \ v1 is set
3 /\ 1 is set
v1 is Element of bool 3
v1 ` is Element of bool 3
3 \ v1 is set
3 /\ 2 is set
v1 is Element of bool 3
v1 ` is Element of bool 3
3 \ v1 is set
v1 is Element of bool 3
v1 ` is Element of bool 3
3 \ v1 is set
v1 is Element of bool 3
v1 ` is Element of bool 3
3 \ v1 is set
v1 is Element of bool 3
v1 ` is Element of bool 3
3 \ v1 is set
y is Element of the carrier of (latt ())
e is Element of bool 3
e ` is Element of bool 3
3 \ e is set
bool [: the carrier of (latt ()), the carrier of (latt ()):] is non empty set
v2 is V1() Function-like V18( the carrier of (latt ()), the carrier of (latt ())) Element of bool [: the carrier of (latt ()), the carrier of (latt ()):]
v2 is V1() Function-like V18( the carrier of (latt ()), the carrier of (latt ())) Element of bool [: the carrier of (latt ()), the carrier of (latt ()):]
OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #) is strict OrthoLattStr
the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #) is set
the L_join of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #) is V1() Function-like V18([: the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):], the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #)) Element of bool [:[: the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):], the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):]
[: the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):] is V1() set
[:[: the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):], the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):] is V1() set
bool [:[: the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):], the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):] is non empty set
the L_meet of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #) is V1() Function-like V18([: the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):], the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #)) Element of bool [:[: the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):], the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):]
LattStr(# the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the L_join of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the L_meet of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #) #) is strict LattStr
the Compl of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #) is V1() Function-like V18( the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #)) Element of bool [: the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):]
bool [: the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #), the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #):] is non empty set
v1 is Element of the carrier of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #)
y is Element of bool 3
the Compl of OrthoLattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()),v2 #) . v1 is set
y ` is Element of bool 3
3 \ y is set
L is strict OrthoLattStr
the carrier of L is 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() set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() 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 strict LattStr
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
L9 is strict OrthoLattStr
the carrier of L9 is 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() set
[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is V1() 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:]
LattStr(# the carrier of L9, the L_join of L9, the L_meet of L9 #) is strict LattStr
the Compl of L9 is V1() Function-like V18( the carrier of L9, the carrier of L9) Element of bool [: the carrier of L9, the carrier of L9:]
bool [: the carrier of L9, the carrier of L9:] is non empty set
v1 is Element of the carrier of L
the Compl of L . v1 is set
the Compl of L9 . v1 is set
y is Element of bool 3
y ` is Element of bool 3
3 \ y is set
() is strict OrthoLattStr
the carrier of () is set
the L_join of () is V1() Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is V1() set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is V1() set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the L_meet of () is V1() Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
LattStr(# the carrier of (), the L_join of (), the L_meet of () #) is strict LattStr
the L_join of (latt ()) is V1() Function-like V18([: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ())) Element of bool [:[: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ()):]
[: the carrier of (latt ()), the carrier of (latt ()):] is V1() non empty set
[:[: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ()):] is V1() non empty set
bool [:[: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ()):] is non empty set
the L_meet of (latt ()) is V1() Function-like V18([: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ())) Element of bool [:[: the carrier of (latt ()), the carrier of (latt ()):], the carrier of (latt ()):]
LattStr(# the carrier of (latt ()), the L_join of (latt ()), the L_meet of (latt ()) #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing LattStr
LattPOSet (latt ()) is strict reflexive transitive antisymmetric with_suprema with_infima RelStr
LattRel (latt ()) is V1() V14( the carrier of (latt ())) V157() V160() V164() Element of bool [: the carrier of (latt ()), the carrier of (latt ()):]
bool [: the carrier of (latt ()), the carrier of (latt ()):] is non empty set
RelStr(# the carrier of (latt ()),(LattRel (latt ())) #) is strict RelStr
the carrier of () is non empty set
the InternalRel of () is V1() Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is V1() non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (), the InternalRel of () #) is strict RelStr
L is set
{0,1,2} is non empty set
L is set
the L_join of () is V1() Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is V1() non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is V1() non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the L_meet of () is V1() Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
LattStr(# the carrier of (), the L_join of (), the L_meet of () #) is non empty strict LattStr
the L_join of () is V1() Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is V1() non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is V1() non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the L_meet of () is V1() Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
LattStr(# the carrier of (), the L_join of (), the L_meet of () #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing LattStr
LattPOSet LattStr(# the carrier of (), the L_join of (), the L_meet of () #) is strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of LattStr(# the carrier of (), the L_join of (), the L_meet of () #) is non empty set
LattRel LattStr(# the carrier of (), the L_join of (), the L_meet of () #) is V1() V14( the carrier of LattStr(# the carrier of (), the L_join of (), the L_meet of () #)) V157() V160() V164() Element of bool [: the carrier of LattStr(# the carrier of (), the L_join of (), the L_meet of () #), the carrier of LattStr(# the carrier of (), the L_join of (), the L_meet of () #):]
[: the carrier of LattStr(# the carrier of (), the L_join of (), the L_meet of () #), the carrier of LattStr(# the carrier of (), the L_join of (), the L_meet of () #):] is V1() non empty set
bool [: the carrier of LattStr(# the carrier of (), the L_join of (), the L_meet of () #), the carrier of LattStr(# the carrier of (), the L_join of (), the L_meet of () #):] is non empty set
RelStr(# the carrier of LattStr(# the carrier of (), the L_join of (), the L_meet of () #),(LattRel LattStr(# the carrier of (), the L_join of (), the L_meet of () #)) #) is strict RelStr
LattPOSet (latt ()) is strict reflexive transitive antisymmetric with_suprema with_infima RelStr
LattRel (latt ()) is V1() V14( the carrier of (latt ())) V157() V160() V164() Element of bool [: the carrier of (latt ()), the carrier of (latt ()):]
[: the carrier of (latt ()), the carrier of (latt ()):] is V1() non empty set
bool [: the carrier of (latt ()), the carrier of (latt ()):] is non empty set
RelStr(# the carrier of (latt ()),(LattRel (latt ())) #) is strict RelStr
the carrier of () is non empty set
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 is Element of the carrier of ()
c is Element of the carrier of ()
LattPOSet () is strict reflexive transitive antisymmetric with_suprema with_infima RelStr
LattRel () is V1() V14( the carrier of ()) V157() V160() V164() Element of bool [: the carrier of (), the carrier of ():]
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),(LattRel ()) #) is strict RelStr
L9 % is Element of the carrier of (LattPOSet ())
the carrier of (LattPOSet ()) is set
c % is Element of the carrier of (LattPOSet ())
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "\/" L9 is Element of the carrier of ()
L "/\" L9 is Element of the carrier of ()
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L9 "\/" c is Element of the carrier of ()
the L_join of () . (L9,c) is Element of the carrier of ()
L9 "/\" c is Element of the carrier of ()
the L_meet of () . (L9,c) is Element of the carrier of ()
v2 is Element of the carrier of ()
v1 is Element of the carrier of ()
y is Element of the carrier of ()
v1 is Element of the carrier of ()
y is Element of the carrier of ()
e is Element of the carrier of ()
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L9 "\/" c is Element of the carrier of ()
L9 "/\" c is Element of the carrier of ()
L is Element of the carrier of ()
v2 is Element of the carrier of ()
L9 is Element of the carrier of ()
v2 is Element of the carrier of ()
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L9 "\/" c is Element of the carrier of ()
L9 "/\" c is Element of the carrier of ()
L is Element of the carrier of ()
v2 is Element of the carrier of ()
L9 is Element of the carrier of ()
v2 is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 "\/" L9 is Element of the carrier of ()
L9 "/\" L9 is Element of the carrier of ()
1 \/ (3 \ 1) is non empty set
1 \/ 3 is non empty set
L is Element of the carrier of ()
c is Element of the carrier of ()
L9 \/ L9 is set
L9 /\ L9 is set
c is Element of the carrier of ()
v2 is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 "\/" L9 is Element of the carrier of ()
L9 "/\" L9 is Element of the carrier of ()
2 \/ (3 \ 2) is non empty set
2 \/ 3 is non empty set
L is Element of the carrier of ()
c is Element of the carrier of ()
L9 \/ L9 is set
L9 /\ L9 is set
c is Element of the carrier of ()
v2 is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "\/" L9 is Element of the carrier of ()
the L_join of () . (L,L9) is Element of the carrier of ()
L "/\" L9 is Element of the carrier of ()
the L_meet of () . (L,L9) is Element of the carrier of ()
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L9 "\/" c is Element of the carrier of ()
L9 "/\" c is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "\/" L9 is Element of the carrier of ()
the L_join of () . (L,L9) is Element of the carrier of ()
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L9 "\/" c is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "\/" L9 is Element of the carrier of ()
the L_join of () . (L,L9) is Element of the carrier of ()
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L9 "\/" c is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "\/" L9 is Element of the carrier of ()
the L_join of () . (L,L9) is Element of the carrier of ()
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L9 "\/" c is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 ` is Element of the carrier of ()
the Compl of () is V1() Function-like V18( the carrier of (), the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
bool [: the carrier of (), the carrier of ():] is non empty set
the Compl of () . L9 is Element of the carrier of ()
L9 is Element of bool 3
L9 ` is Element of bool 3
3 \ L9 is set
{0} is non empty set
{1} is non empty set
{2} is non empty set
{0,1} is non empty set
{1,2} is non empty set
{0,2} is non empty set
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "/\" L9 is Element of the carrier of ()
the L_meet of () . (L,L9) is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "\/" L9 is Element of the carrier of ()
the L_join of () . (L,L9) is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "\/" L9 is Element of the carrier of ()
the L_join of () . (L,L9) is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "/\" L9 is Element of the carrier of ()
the L_meet of () . (L,L9) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 "/\" L is Element of the carrier of ()
the L_meet of () . (L9,L) is Element of the carrier of ()
L9 is Element of the carrier of ()
L "/\" L9 is Element of the carrier of ()
the L_meet of () . (L,L9) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 "/\" L is Element of the carrier of ()
the L_meet of () . (L9,L) is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "\/" L9 is Element of the carrier of ()
the L_join of () . (L,L9) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 "\/" L is Element of the carrier of ()
the L_join of () . (L9,L) is Element of the carrier of ()
L9 is Element of the carrier of ()
L "\/" L9 is Element of the carrier of ()
the L_join of () . (L,L9) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 "\/" L is Element of the carrier of ()
the L_join of () . (L9,L) is Element of the carrier of ()
Top () is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "\/" L9 is Element of the carrier of ()
the L_join of () . (L,L9) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 "\/" L is Element of the carrier of ()
the L_join of () . (L9,L) is Element of the carrier of ()
Bottom () is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L "/\" L9 is Element of the carrier of ()
the L_meet of () . (L,L9) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 "/\" L is Element of the carrier of ()
the L_meet of () . (L9,L) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 ` is Element of the carrier of ()
the Compl of () is V1() Function-like V18( the carrier of (), the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
bool [: the carrier of (), the carrier of ():] is non empty set
the Compl of () . L9 is Element of the carrier of ()
(L9 `) ` is Element of the carrier of ()
the Compl of () . (L9 `) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 ` is Element of the carrier of ()
the Compl of () is V1() Function-like V18( the carrier of (), the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
bool [: the carrier of (), the carrier of ():] is non empty set
the Compl of () . L9 is Element of the carrier of ()
L9 "\/" (L9 `) is Element of the carrier of ()
the L_join of () . (L9,(L9 `)) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 ` is Element of the carrier of ()
the Compl of () is V1() Function-like V18( the carrier of (), the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
bool [: the carrier of (), the carrier of ():] is non empty set
the Compl of () . L9 is Element of the carrier of ()
L9 "\/" (L9 `) is Element of the carrier of ()
the L_join of () . (L9,(L9 `)) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 ` is Element of the carrier of ()
the Compl of () . L9 is Element of the carrier of ()
L9 "\/" (L9 `) is Element of the carrier of ()
the L_join of () . (L9,(L9 `)) is Element of the carrier of ()
L9 "\/" (L9 `) is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 is Element of the carrier of ()
L9 ` is Element of the carrier of ()
the Compl of () is V1() Function-like V18( the carrier of (), the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
bool [: the carrier of (), the carrier of ():] is non empty set
the Compl of () . L9 is Element of the carrier of ()
L9 ` is Element of the carrier of ()
the Compl of () . L9 is Element of the carrier of ()
bool {0,1,2} is non empty set
c is Element of bool {0,1,2}
v2 is Element of bool {0,1,2}
v1 is Element of bool 3
y is Element of bool 3
y ` is Element of bool 3
3 \ y is set
v1 ` is Element of bool 3
3 \ v1 is set
v2 is set
L9 is Element of the carrier of ()
c is Element of the carrier of ()
L9 ` is Element of the carrier of ()
the Compl of () is V1() Function-like V18( the carrier of (), the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
bool [: the carrier of (), the carrier of ():] is non empty set
the Compl of () . L9 is Element of the carrier of ()
(L9 `) "/\" c is Element of the carrier of ()
the L_meet of () . ((L9 `),c) is Element of the carrier of ()
L9 "\/" ((L9 `) "/\" c) is Element of the carrier of ()
the L_join of () . (L9,((L9 `) "/\" c)) is Element of the carrier of ()
L is Element of the carrier of ()
L9 is Element of the carrier of ()
L ` is Element of the carrier of ()
the Compl of () is V1() Function-like V18( the carrier of (), the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
bool [: the carrier of (), the carrier of ():] is non empty set
the Compl of () . L is Element of the carrier of ()
(L `) "/\" L9 is Element of the carrier of ()
the L_meet of () . ((L `),L9) is Element of the carrier of ()
L "\/" ((L `) "/\" L9) is Element of the carrier of ()
the L_join of () . (L,((L `) "/\" L9)) is Element of the carrier of ()
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the carrier of L is non empty set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the carrier of L is non empty set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the carrier of L is non empty set
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_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
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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the carrier of L is non empty set
c is Element of the carrier of L
v2 is Element of the carrier of L
v2 ` 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 . v2 is Element of the carrier of L
(v2 `) ` is Element of the carrier of L
the Compl of L . (v2 `) 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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top 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
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 "\/" 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,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
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_meet of L . (L9,(c `)) is Element of the carrier of L
(L9 `) "/\" (c `) is Element of the carrier of L
the L_meet of L . ((L9 `),(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 "/\" c) ` is Element of the carrier of L
the Compl of L . (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 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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the carrier of L is non empty set
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 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
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 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 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
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 "\/" ((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 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_meet of L . (((L9 "\/" ((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 `) "/\" 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 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_meet of L . (L9,((((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 `) `) "\/" ((((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_meet 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_meet 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
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 `) `) "\/" (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 `)) 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 `) `) "\/" (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 `) 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 "\/" (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 `) 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_meet of L . ((L9 "/\" (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 "\/" (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 `)) ` 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_meet of L . (((L9 "\/" (L9 `)) `),(L9 "\/" (L9 `))) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top OrthoLattStr
the carrier of L is non empty set
Top L 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 `) "/\" (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 `) ` 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 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_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
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
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
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 "\/" ((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 is Element of the carrier of L
the L_join 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 . (((L9 `) "\/" 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 `) "/\" 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 `) `)) ` 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 . (((((L9 `) "\/" ((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 `) "/\" L9) is Element of the carrier of L
the L_join of L . (((L9 "/\" (L9 `)) `),((L9 `) "/\" L9)) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top 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 ` 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 `) "\/" 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
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 `) `) "/\" (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 `) ` 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 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 `) "\/" 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 Compl 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
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 `) ` 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_meet 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_meet of L . ((L9 `),(((((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 `) "/\" (((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 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 `) "/\" 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_join 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_join 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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top 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
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
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 `) "\/" (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
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
(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 "/\" 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_meet of L . (L9,((L9 `) "\/" (L9 "/\" L9))) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top 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
(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
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) "/\" (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) "\/" ((L9 "\/" L9) "/\" (L9 `)) is Element of the carrier of L
the L_join of L . (((L9 "\/" 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_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 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 L_meet of L . ((L9 "\/" L9),(L9 `)) is Element of the carrier of L
((L9 "\/" L9) "/\" L9) "\/" ((L9 "\/" L9) "/\" (L9 `)) is Element of the carrier of L
the L_join of L . (((L9 "\/" L9) "/\" L9),((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 "\/" 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 `) 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 . ((L9 "/\" L9),(L9 "/\" (L9 `))) is Element of the carrier 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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top 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
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
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_join of L . (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 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 "\/" (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_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 . ((L9 "/\" 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 L_meet of L . ((L9 "\/" L9),(L9 `)) is Element of the carrier of L
((L9 "\/" L9) "/\" L9) "\/" ((L9 "\/" L9) "/\" (L9 `)) is Element of the carrier of L
the L_join of L . (((L9 "\/" L9) "/\" L9),((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 "\/" 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_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
(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 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 "\/" 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 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_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 . ((L9 "/\" L9),(L9 "/\" (L9 `))) is Element of the carrier 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_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
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 "\/" c is Element of the carrier of L
the L_join of L . (L9,c) is Element of the carrier of L
(L9 "\/" L9) "/\" (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 "\/" 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 "\/" 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 "\/" c)) "\/" ((L9 "\/" L9) "/\" (L9 `)) is Element of the carrier of L
the L_join of L . (((L9 "\/" L9) "/\" (L9 "\/" c)),((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 "\/" c) "/\" (L9 "\/" L9) is Element of the carrier of L
the L_meet of L . ((L9 "\/" c),(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 `)) "\/" ((L9 "\/" L9) "/\" L9) is Element of the carrier of L
the L_join of L . (((L9 "\/" L9) "/\" (L9 `)),((L9 "\/" L9) "/\" L9)) is Element of the carrier of L
((L9 "\/" L9) "/\" (L9 `)) "\/" ((L9 "\/" L9) "/\" (L9 "\/" c)) is Element of the carrier of L
the L_join of L . (((L9 "\/" L9) "/\" (L9 `)),((L9 "\/" L9) "/\" (L9 "\/" c))) is Element of the carrier of L
((L9 "\/" L9) "/\" L9) "\/" ((L9 "\/" L9) "/\" (L9 `)) is Element of the carrier of L
the L_join of L . (((L9 "\/" 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
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
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
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) "/\" (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) "\/" ((L9 "\/" L9) "/\" (L9 `)) is Element of the carrier of L
the L_join of L . (((L9 "\/" L9) "/\" L9),((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 "\/" (L9 "/\" (L9 `))) is Element of the carrier of L
the L_meet of L . ((L9 "\/" L9),(L9 "\/" (L9 "/\" (L9 `)))) is Element of the carrier of L
((L9 "\/" L9) "/\" (L9 "\/" (L9 "/\" (L9 `)))) "\/" ((L9 "\/" L9) "/\" (L9 `)) is Element of the carrier of L
the L_join of L . (((L9 "\/" L9) "/\" (L9 "\/" (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
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
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 . (L9,(L9 "/\" (L9 `))) is Element of the carrier of L
(L9 "\/" (L9 "/\" (L9 `))) "/\" (L9 "\/" L9) is Element of the carrier of L
the L_meet 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 "\/" L9)) "\/" ((L9 "\/" (L9 "/\" (L9 `))) "/\" (L9 `)) is Element of the carrier of L
the L_join of L . (((L9 "\/" (L9 "/\" (L9 `))) "/\" (L9 "\/" L9)),((L9 "\/" (L9 "/\" (L9 `))) "/\" (L9 `))) is Element of the carrier of L
(L9 "/\" (L9 "\/" L9)) "\/" ((L9 "\/" (L9 "/\" (L9 `))) "/\" (L9 `)) is Element of the carrier of L
the L_join of L . ((L9 "/\" (L9 "\/" L9)),((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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan join-Associative meet-Associative meet-Absorbing () () 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
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
L9 ` is Element of the carrier of L
the Compl of L . L9 is Element of the carrier of L
H1(L9) "\/" H1(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
(H1(L9) "\/" H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(L9) "\/" H1(L9)) is Element of the carrier of L
L9 "\/" H1(H1(L9) "\/" H1(L9)) is Element of the carrier of L
the L_join of L . (L9,((H1(L9) "\/" H1(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 ` 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
H1(L9) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
L9 "\/" H1(H1(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,(H1(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
H1(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
c ` is Element of the carrier of L
the Compl of L . c is Element of the carrier of L
H1(H1(L9)) "\/" H1(c) is Element of the carrier of L
the L_join of L . ((H1(L9) `),(c `)) is Element of the carrier of L
(H1(H1(L9)) "\/" H1(c)) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) "\/" H1(c)) is Element of the carrier of L
H1(L9) "\/" H1(H1(H1(L9)) "\/" H1(c)) is Element of the carrier of L
the L_join of L . ((L9 `),((H1(H1(L9)) "\/" H1(c)) `)) is Element of the carrier of L
L9 "\/" H1(H1(L9)) is Element of the carrier of L
the L_join of L . (L9,(H1(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
H1(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 "\/" 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 Compl of L . (L9 "\/" L9) is Element of the carrier of L
H1(H1(L9)) "\/" H1(L9 "\/" L9) is Element of the carrier of L
the L_join of L . ((H1(L9) `),((L9 "\/" L9) `)) is Element of the carrier of L
(H1(H1(L9)) "\/" H1(L9 "\/" L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) "\/" H1(L9 "\/" L9)) is Element of the carrier of L
L9 "\/" H1(H1(H1(L9)) "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . (L9,((H1(H1(L9)) "\/" H1(L9 "\/" L9)) `)) is Element of the carrier of L
H1(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
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
H1(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
(H1(L9) "\/" L9) ` is Element of the carrier of L
the Compl of L . (H1(L9) "\/" L9) is Element of the carrier of L
L9 "\/" H1(H1(L9) "\/" L9) is Element of the carrier of L
the L_join of L . (L9,((H1(L9) "\/" L9) `)) is Element of the carrier of L
H1(L9) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
H1(H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(L9) `) is Element of the carrier of L
H1(H1(H1(L9))) "\/" H1(H1(L9) "\/" L9) is Element of the carrier of L
the L_join of L . ((H1(H1(L9)) `),((H1(L9) "\/" L9) `)) is Element of the carrier of L
(H1(H1(H1(L9))) "\/" H1(H1(L9) "\/" L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(H1(L9))) "\/" H1(H1(L9) "\/" L9)) is Element of the carrier of L
H1(L9) "\/" H1(H1(H1(H1(L9))) "\/" H1(H1(L9) "\/" L9)) is Element of the carrier of L
the L_join of L . ((L9 `),((H1(H1(H1(L9))) "\/" H1(H1(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
c is Element of the carrier of L
H1(L9) "\/" c is Element of the carrier of L
the L_join of L . ((L9 `),c) is Element of the carrier of L
(H1(L9) "\/" c) ` is Element of the carrier of L
the Compl of L . (H1(L9) "\/" c) is Element of the carrier of L
L9 "\/" H1(H1(L9) "\/" c) is Element of the carrier of L
the L_join of L . (L9,((H1(L9) "\/" c) `)) is Element of the carrier of L
L9 "\/" (L9 "\/" H1(H1(L9) "\/" c)) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" H1(H1(L9) "\/" c))) is Element of the carrier of L
L9 "\/" H1(H1(L9) "\/" c) is Element of the carrier of L
the L_join of L . (L9,((H1(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
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
H1(L9) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
L9 "\/" H1(H1(L9)) is Element of the carrier of L
the L_join of L . (L9,(H1(L9) `)) is Element of the carrier of L
L9 "\/" (L9 "\/" H1(H1(L9))) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" H1(H1(L9)))) is Element of the carrier of L
L9 "\/" H1(H1(L9)) is Element of the carrier of L
the L_join of L . (L9,(H1(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 `) `) ` 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 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 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 `) `) ` 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 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_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 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 `) `) ` 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 `) `) `) ` 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
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 `) `) ` 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 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
H1(L9) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
H1(H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(L9) `) is Element of the carrier of L
H1(H1(H1(L9))) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) `) is Element of the carrier of L
H1(H1(H1(H1(L9)))) ` is Element of the carrier of L
the Compl of L . (H1(H1(H1(L9))) `) is Element of the carrier of L
H1(H1(H1(H1(H1(L9))))) ` is Element of the carrier of L
the Compl of L . (H1(H1(H1(H1(L9)))) `) is Element of the carrier of L
H1(H1(H1(H1(H1(H1(L9)))))) "\/" H1(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 . ((H1(H1(H1(H1(H1(L9))))) `),(L9 `)) is Element of the carrier of L
(H1(H1(H1(H1(H1(H1(L9)))))) "\/" H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(H1(H1(H1(H1(L9)))))) "\/" H1(L9)) is Element of the carrier of L
H1(H1(H1(H1(L9)))) "\/" H1(H1(H1(H1(H1(H1(H1(L9)))))) "\/" H1(L9)) is Element of the carrier of L
the L_join of L . ((H1(H1(H1(L9))) `),((H1(H1(H1(H1(H1(H1(L9)))))) "\/" H1(L9)) `)) is Element of the carrier of L
H1(H1(H1(H1(L9)))) "\/" L9 is Element of the carrier of L
the L_join of L . ((H1(H1(H1(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
H1(L9) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
H1(H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(L9) `) is Element of the carrier of L
H1(H1(H1(L9))) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) `) is Element of the carrier of L
H1(H1(H1(H1(L9)))) ` is Element of the carrier of L
the Compl of L . (H1(H1(H1(L9))) `) is Element of the carrier of L
H1(H1(H1(H1(H1(L9))))) ` is Element of the carrier of L
the Compl of L . (H1(H1(H1(H1(L9)))) `) is Element of the carrier of L
H1(H1(H1(H1(H1(H1(L9)))))) "\/" H1(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 . ((H1(H1(H1(H1(H1(L9))))) `),(L9 `)) is Element of the carrier of L
(H1(H1(H1(H1(H1(H1(L9)))))) "\/" H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(H1(H1(H1(H1(L9)))))) "\/" H1(L9)) is Element of the carrier of L
H1(H1(L9)) "\/" H1(H1(H1(H1(H1(H1(H1(L9)))))) "\/" H1(L9)) is Element of the carrier of L
the L_join of L . ((H1(L9) `),((H1(H1(H1(H1(H1(H1(L9)))))) "\/" H1(L9)) `)) is Element of the carrier of L
H1(H1(H1(H1(L9)))) "\/" L9 is Element of the carrier of L
the L_join of L . ((H1(H1(H1(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 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
H1(L9) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
H1(H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(L9) `) is Element of the carrier of L
H1(H1(H1(L9))) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) `) is Element of the carrier of L
H1(H1(H1(H1(L9)))) "\/" H1(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 . ((H1(H1(H1(L9))) `),(L9 `)) is Element of the carrier of L
(H1(H1(H1(H1(L9)))) "\/" H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(H1(H1(L9)))) "\/" H1(L9)) is Element of the carrier of L
H1(H1(L9)) "\/" H1(H1(H1(H1(H1(L9)))) "\/" H1(L9)) is Element of the carrier of L
the L_join of L . ((H1(L9) `),((H1(H1(H1(H1(L9)))) "\/" H1(L9)) `)) is Element of the carrier of L
H1(H1(H1(H1(L9)))) "\/" L9 is Element of the carrier of L
the L_join of L . ((H1(H1(H1(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 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
H1(L9) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
H1(H1(L9)) "\/" H1(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 . ((H1(L9) `),(L9 `)) is Element of the carrier of L
(H1(H1(L9)) "\/" H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) "\/" H1(L9)) is Element of the carrier of L
H1(H1(L9)) "\/" H1(H1(H1(L9)) "\/" H1(L9)) is Element of the carrier of L
the L_join of L . ((H1(L9) `),((H1(H1(L9)) "\/" H1(L9)) `)) is Element of the carrier of L
H1(H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(L9) `) is Element of the carrier of L
H1(H1(H1(L9))) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) `) is Element of the carrier of L
H1(H1(H1(H1(L9)))) "\/" L9 is Element of the carrier of L
the L_join of L . ((H1(H1(H1(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 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
H1(L9) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
H1(H1(L9)) "\/" H1(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 . ((H1(L9) `),(L9 `)) is Element of the carrier of L
(H1(H1(L9)) "\/" H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) "\/" H1(L9)) is Element of the carrier of L
H1(H1(L9)) "\/" H1(H1(H1(L9)) "\/" H1(L9)) is Element of the carrier of L
the L_join of L . ((H1(L9) `),((H1(H1(L9)) "\/" H1(L9)) `)) is Element of the carrier of L
H1(H1(L9)) "\/" L9 is Element of the carrier of L
the L_join of L . ((H1(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 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
H1(L9) ` is Element of the carrier of L
the Compl of L . (L9 `) is Element of the carrier of L
H1(H1(L9)) "\/" H1(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 . ((H1(L9) `),(L9 `)) is Element of the carrier of L
(H1(H1(L9)) "\/" H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) "\/" H1(L9)) is Element of the carrier of L
H1(H1(L9)) "\/" H1(H1(H1(L9)) "\/" H1(L9)) is Element of the carrier of L
the L_join of L . ((H1(L9) `),((H1(H1(L9)) "\/" H1(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 . (((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
H1(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
L9 "\/" H1(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 "\/" H1(L9)) ` is Element of the carrier of L
the Compl of L . (L9 "\/" H1(L9)) is Element of the carrier of L
H1(H1(L9)) "\/" H1(L9 "\/" H1(L9)) is Element of the carrier of L
the L_join of L . ((H1(L9) `),((L9 "\/" H1(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
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
H1(L9) ` is Element of the carrier of L
H1(H1(L9)) "\/" H1(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 . ((H1(L9) `),(L9 `)) is Element of the carrier of L
(H1(H1(L9)) "\/" H1(L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) "\/" H1(L9)) is Element of the carrier of L
H1(H1(L9)) "\/" H1(H1(H1(L9)) "\/" H1(L9)) is Element of the carrier of L
the L_join of L . ((H1(L9) `),((H1(H1(L9)) "\/" H1(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
H1(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 "\/" 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 Compl of L . (L9 "\/" L9) is Element of the carrier of L
H1(H1(L9)) "\/" H1(L9 "\/" L9) is Element of the carrier of L
the L_join of L . ((H1(L9) `),((L9 "\/" L9) `)) is Element of the carrier of L
(H1(H1(L9)) "\/" H1(L9 "\/" L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) "\/" H1(L9 "\/" L9)) is Element of the carrier of L
L9 "\/" H1(H1(H1(L9)) "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . (L9,((H1(H1(L9)) "\/" H1(L9 "\/" L9)) `)) is Element of the carrier of L
L9 "\/" H1(H1(L9)) is Element of the carrier of L
the L_join of L . (L9,(H1(L9) `)) is Element of the carrier of L
L9 "\/" (L9 "\/" H1(H1(L9))) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" H1(H1(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
H1(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 "\/" 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 Compl of L . (L9 "\/" L9) is Element of the carrier of L
H1(H1(L9)) "\/" H1(L9 "\/" L9) is Element of the carrier of L
the L_join of L . ((H1(L9) `),((L9 "\/" L9) `)) is Element of the carrier of L
(H1(H1(L9)) "\/" H1(L9 "\/" L9)) ` is Element of the carrier of L
the Compl of L . (H1(H1(L9)) "\/" H1(L9 "\/" L9)) is Element of the carrier of L
L9 "\/" H1(H1(H1(L9)) "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . (L9,((H1(H1(L9)) "\/" H1(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_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 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 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 "\/" L9) is Element of the carrier of L
L9 "\/" H1(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 "\/" H1(L9 "\/" L9)) ` is Element of the carrier of L
the Compl of L . (L9 "\/" H1(L9 "\/" L9)) is Element of the carrier of L
L9 "\/" H1(L9 "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . (L9,((L9 "\/" H1(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 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
H1(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 "\/" H1(L9) is Element of the carrier of L
the L_join of L . (L9,(L9 `)) is Element of the carrier of L
L9 "\/" (L9 "\/" H1(L9)) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" H1(L9))) is Element of the carrier of L
(L9 "\/" H1(L9)) ` is Element of the carrier of L
the Compl of L . (L9 "\/" H1(L9)) is Element of the carrier of L
H1(L9) "\/" H1(L9 "\/" H1(L9)) is Element of the carrier of L
the L_join of L . ((L9 `),((L9 "\/" H1(L9)) `)) is Element of the carrier of L
(H1(L9) "\/" H1(L9 "\/" H1(L9))) ` is Element of the carrier of L
the Compl of L . (H1(L9) "\/" H1(L9 "\/" H1(L9))) is Element of the carrier of L
H1(L9) "\/" H1(H1(L9) "\/" H1(L9 "\/" H1(L9))) is Element of the carrier of L
the L_join of L . ((L9 `),((H1(L9) "\/" H1(L9 "\/" H1(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
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 Compl of L . (L9 "\/" L9) is Element of the carrier of L
H1(L9) "\/" H1(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 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
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) "\/" H1(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 Compl of L . (L9 "\/" L9) is Element of the carrier of L
H1(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 `) "\/" H1(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
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
L9 "\/" H1(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 "\/" H1(L9)) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" H1(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
H1(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) "\/" H1(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 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 "\/" L9) is Element of the carrier of L
H1(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
c is Element of the carrier of L
c "\/" H1(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 "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . (L9,(c "\/" H1(L9 "\/" L9))) is Element of the carrier of L
L9 "\/" (L9 "\/" (c "\/" H1(L9 "\/" L9))) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" (c "\/" H1(L9 "\/" L9)))) is Element of the carrier of L
(L9 "\/" L9) "\/" (c "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . ((L9 "\/" L9),(c "\/" H1(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
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 Compl of L . (L9 "\/" L9) is Element of the carrier of L
L9 "\/" H1(L9) is Element of the carrier of L
the L_join of L . (L9,(L9 `)) is Element of the carrier of L
L9 "\/" (L9 "\/" H1(L9)) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" H1(L9))) is Element of the carrier of L
c is Element of the carrier of L
c "\/" H1(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 "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . (L9,(c "\/" H1(L9 "\/" L9))) is Element of the carrier of L
L9 "\/" (L9 "\/" (c "\/" H1(L9 "\/" L9))) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" (c "\/" H1(L9 "\/" L9)))) is Element of the carrier of L
H1(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_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 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 "\/" 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
H1(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) ` is Element of the carrier of L
the Compl of L . (L9 "\/" L9) is Element of the carrier of L
c is Element of the carrier of L
c "\/" H1(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 "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . (L9,(c "\/" H1(L9 "\/" L9))) is Element of the carrier of L
L9 "\/" (L9 "\/" (c "\/" H1(L9 "\/" L9))) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" (c "\/" H1(L9 "\/" L9)))) is Element of the carrier of L
(L9 "\/" L9) "\/" (c "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . ((L9 "\/" L9),(c "\/" H1(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 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 "\/" 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
H1(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
the Compl of L . L9 is Element of the carrier of L
L9 "\/" H1(L9) is Element of the carrier of L
the L_join of L . (L9,(L9 `)) is Element of the carrier of L
L9 "\/" (L9 "\/" H1(L9)) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" H1(L9))) is Element of the carrier of L
v1 is Element of the carrier of L
v2 is Element of the carrier of L
c is Element of the carrier of L
v1 "\/" v2 is Element of the carrier of L
the L_join of L . (v1,v2) is Element of the carrier of L
(v1 "\/" v2) ` is Element of the carrier of L
the Compl of L . (v1 "\/" v2) is Element of the carrier of L
c "\/" H1(v1 "\/" v2) is Element of the carrier of L
the L_join of L . (c,((v1 "\/" v2) `)) is Element of the carrier of L
v2 "\/" (c "\/" H1(v1 "\/" v2)) is Element of the carrier of L
the L_join of L . (v2,(c "\/" H1(v1 "\/" v2))) is Element of the carrier of L
v1 "\/" (v2 "\/" (c "\/" H1(v1 "\/" v2))) is Element of the carrier of L
the L_join of L . (v1,(v2 "\/" (c "\/" H1(v1 "\/" v2)))) is Element of the carrier of L
v1 ` is Element of the carrier of L
the Compl of L . v1 is Element of the carrier of L
v2 "\/" H1(v1) is Element of the carrier of L
the L_join of L . (v2,(v1 `)) is Element of the carrier of L
v1 "\/" (v2 "\/" H1(v1)) is Element of the carrier of L
the L_join of L . (v1,(v2 "\/" H1(v1))) is Element of the carrier of L
v2 "\/" v1 is Element of the carrier of L
the L_join of L . (v2,v1) is Element of the carrier of L
(v2 "\/" v1) ` is Element of the carrier of L
the Compl of L . (v2 "\/" v1) is Element of the carrier of L
H1(v2 "\/" v1) "\/" (v1 "\/" v2) is Element of the carrier of L
the L_join of L . (((v2 "\/" v1) `),(v1 "\/" v2)) 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
L9 "\/" H1(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 "\/" H1(L9)) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" H1(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
c is Element of the carrier of L
c "\/" H1(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 "\/" L9) "\/" (c "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . ((L9 "\/" L9),(c "\/" H1(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
H1(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
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_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
c is Element of the carrier of L
c "\/" H1(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 "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . (L9,(c "\/" H1(L9 "\/" L9))) is Element of the carrier of L
L9 "\/" (L9 "\/" (c "\/" H1(L9 "\/" L9))) is Element of the carrier of L
the L_join of L . (L9,(L9 "\/" (c "\/" H1(L9 "\/" L9)))) is Element of the carrier of L
(L9 "\/" L9) "\/" (c "\/" H1(L9 "\/" L9)) is Element of the carrier of L
the L_join of L . ((L9 "\/" L9),(c "\/" H1(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
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_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
v1 is Element of the carrier of L
v2 is Element of the carrier of L
c is Element of the carrier of L
v1 "\/" v2 is Element of the carrier of L
the L_join of L . (v1,v2) is Element of the carrier of L
(v1 "\/" v2) ` is Element of the carrier of L
the Compl of L . (v1 "\/" v2) is Element of the carrier of L
c "\/" H1(v1 "\/" v2) is Element of the carrier of L
the L_join of L . (c,((v1 "\/" v2) `)) is Element of the carrier of L
v2 "\/" (c "\/" H1(v1 "\/" v2)) is Element of the carrier of L
the L_join of L . (v2,(c "\/" H1(v1 "\/" v2))) is Element of the carrier of L
v1 "\/" (v2 "\/" (c "\/" H1(v1 "\/" v2))) is Element of the carrier of L
the L_join of L . (v1,(v2 "\/" (c "\/" H1(v1 "\/" v2)))) is Element of the carrier of L
v1 ` is Element of the carrier of L
the Compl of L . v1 is Element of the carrier of L
v2 "\/" H1(v1) is Element of the carrier of L
the L_join of L . (v2,(v1 `)) is Element of the carrier of L
v1 "\/" (v2 "\/" H1(v1)) is Element of the carrier of L
the L_join of L . (v1,(v2 "\/" H1(v1))) is Element of the carrier of L
v2 ` is Element of the carrier of L
the Compl of L . v2 is Element of the carrier of L
v1 "\/" H1(v2) is Element of the carrier of L
the L_join of L . (v1,(v2 `)) is Element of the carrier of L
v2 "\/" (v1 "\/" H1(v2)) is Element of the carrier of L
the L_join of L . (v2,(v1 "\/" H1(v2))) 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 "\/" (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 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 "\/" H1(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 "\/" H1(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
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
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
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
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 `)) ` 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 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
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 `) `) 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 `) `) "\/" ((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 `) 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 `) "\/" ((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 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 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 "\/" 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_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 `) "/\" (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
(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 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 `) `) ` is Element of the carrier of L
the Compl 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 `) `) `) "\/" (((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 `) "\/" 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
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_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 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 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 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 `) `) ` 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 "\/" (((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 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
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
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 `) `) 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 ` 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 `) `) ` 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 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_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 ` 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 `) `) ` 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 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 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 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 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 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
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 `)) ` 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 `) `) `) ` 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 `) `) `) `) `) ` 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_join 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 `) 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 `) `) `) `) `) `) "\/" (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
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 `)) ` 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 "\/" 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
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_join 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 `) `) "\/" 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 Compl 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
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 "/\" c is Element of the carrier of L
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 ` 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
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 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 `),(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_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 . 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 . ((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 `) "\/" (c `) is Element of the carrier of L
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 `) "\/" (c `))) ` is Element of the carrier of L
the Compl of L . ((L9 `) "\/" ((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 "/\" 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 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing OrthoLattStr
L9 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan join-Associative meet-Associative meet-Absorbing with_Top () () OrthoLattStr