:: ROBBINS4 semantic presentation

REAL is set

NAT is non empty V24() V25() V26() Element of bool REAL

bool REAL is non empty set

NAT is non empty V24() V25() V26() set

bool NAT is non empty set

bool NAT is non empty set

2 is non empty V24() V25() V26() V30() V173() Element of NAT

[:2,2:] is V1() non empty set

[:[:2,2:],2:] is V1() non empty set

bool [:[:2,2:],2:] is non empty set

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