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