:: ROBBINS3 semantic presentation

K97() is V26() V32() cardinal limit_cardinal M2( bool K93())

K93() is set

bool K93() is set

K92() is V26() V32() cardinal limit_cardinal set

bool K92() is V32() set

bool K97() is V32() set

2 is non empty set

[:2,2:] is Relation-like set

[:[:2,2:],2:] is Relation-like set

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

[:K97(),K93():] is Relation-like set

bool [:K97(),K93():] is set

bool (bool K93()) is set

K351() is non empty V245(K93()) V248(K93()) M2( bool (bool K93()))

1 is non empty set

[:1,1:] is Relation-like set

bool [:1,1:] is set

[:[:1,1:],1:] is Relation-like set

bool [:[:1,1:],1:] is set

K451() is set

Probabilities K351() is set

{} is set

{{}} is non empty trivial 1 -element set

L is non empty LattStr

the carrier of L is non empty set

L9 is M2( the carrier of L)

L9 "\/" L9 is M2( the carrier of L)

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_join of L . (L9,L9) is M2( the carrier of L)

L9 "/\" L9 is M2( the carrier of L)

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

the L_meet of L . (L9,L9) is M2( the carrier of L)

L9 "\/" (L9 "/\" L9) is M2( the carrier of L)

the L_join of L . (L9,(L9 "/\" L9)) is M2( the carrier of L)

L9 is M2( the carrier of L)

L9 "/\" L9 is M2( the carrier of L)

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L . (L9,L9) is M2( the carrier of L)

L9 "\/" L9 is M2( the carrier of L)

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

the L_join of L . (L9,L9) is M2( the carrier of L)

L9 "/\" (L9 "\/" L9) is M2( the carrier of L)

the L_meet of L . (L9,(L9 "\/" L9)) is M2( the carrier of L)

L is non empty LattStr

the carrier of L is non empty set

L9 is M2( the carrier of L)

f is M2( the carrier of L)

L9 "/\" f is M2( the carrier of L)

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L . (L9,f) is M2( the carrier of L)

f "/\" L9 is M2( the carrier of L)

the L_meet of L . (f,L9) is M2( the carrier of L)

f "\/" L9 is M2( the carrier of L)

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

the L_join of L . (f,L9) is M2( the carrier of L)

f "/\" (f "\/" L9) is M2( the carrier of L)

the L_meet of L . (f,(f "\/" L9)) is M2( the carrier of L)

L9 "/\" (f "/\" (f "\/" L9)) is M2( the carrier of L)

the L_meet of L . (L9,(f "/\" (f "\/" L9))) is M2( the carrier of L)

L9 "/\" (f "\/" L9) is M2( the carrier of L)

the L_meet of L . (L9,(f "\/" L9)) is M2( the carrier of L)

f "/\" (L9 "/\" (f "\/" L9)) is M2( the carrier of L)

the L_meet of L . (f,(L9 "/\" (f "\/" L9))) is M2( the carrier of L)

L9 "\/" L9 is M2( the carrier of L)

the L_join of L . (L9,L9) is M2( the carrier of L)

f "\/" (L9 "\/" L9) is M2( the carrier of L)

the L_join of L . (f,(L9 "\/" L9)) is M2( the carrier of L)

L9 "/\" (f "\/" (L9 "\/" L9)) is M2( the carrier of L)

the L_meet of L . (L9,(f "\/" (L9 "\/" L9))) is M2( the carrier of L)

f "/\" (L9 "/\" (f "\/" (L9 "\/" L9))) is M2( the carrier of L)

the L_meet of L . (f,(L9 "/\" (f "\/" (L9 "\/" L9)))) is M2( the carrier of L)

L9 "\/" (f "\/" L9) is M2( the carrier of L)

the L_join of L . (L9,(f "\/" L9)) is M2( the carrier of L)

L9 "/\" (L9 "\/" (f "\/" L9)) is M2( the carrier of L)

the L_meet of L . (L9,(L9 "\/" (f "\/" L9))) is M2( the carrier of L)

f "/\" (L9 "/\" (L9 "\/" (f "\/" L9))) is M2( the carrier of L)

the L_meet of L . (f,(L9 "/\" (L9 "\/" (f "\/" L9)))) is M2( the carrier of L)

L9 is M2( the carrier of L)

f is M2( the carrier of L)

L9 "\/" f is M2( the carrier of L)

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_join of L . (L9,f) is M2( the carrier of L)

f "\/" L9 is M2( the carrier of L)

the L_join of L . (f,L9) is M2( the carrier of L)

f "/\" L9 is M2( the carrier of L)

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

the L_meet of L . (f,L9) is M2( the carrier of L)

f "\/" (f "/\" L9) is M2( the carrier of L)

the L_join of L . (f,(f "/\" L9)) is M2( the carrier of L)

L9 "\/" (f "\/" (f "/\" L9)) is M2( the carrier of L)

the L_join of L . (L9,(f "\/" (f "/\" L9))) is M2( the carrier of L)

L9 "\/" (f "/\" L9) is M2( the carrier of L)

the L_join of L . (L9,(f "/\" L9)) is M2( the carrier of L)

f "\/" (L9 "\/" (f "/\" L9)) is M2( the carrier of L)

the L_join of L . (f,(L9 "\/" (f "/\" L9))) is M2( the carrier of L)

L9 "/\" L9 is M2( the carrier of L)

the L_meet of L . (L9,L9) is M2( the carrier of L)

f "/\" (L9 "/\" L9) is M2( the carrier of L)

the L_meet of L . (f,(L9 "/\" L9)) is M2( the carrier of L)

L9 "\/" (f "/\" (L9 "/\" L9)) is M2( the carrier of L)

the L_join of L . (L9,(f "/\" (L9 "/\" L9))) is M2( the carrier of L)

f "\/" (L9 "\/" (f "/\" (L9 "/\" L9))) is M2( the carrier of L)

the L_join of L . (f,(L9 "\/" (f "/\" (L9 "/\" L9)))) is M2( the carrier of L)

L9 "/\" (f "/\" L9) is M2( the carrier of L)

the L_meet of L . (L9,(f "/\" L9)) is M2( the carrier of L)

L9 "\/" (L9 "/\" (f "/\" L9)) is M2( the carrier of L)

the L_join of L . (L9,(L9 "/\" (f "/\" L9))) is M2( the carrier of L)

f "\/" (L9 "\/" (L9 "/\" (f "/\" L9))) is M2( the carrier of L)

the L_join of L . (f,(L9 "\/" (L9 "/\" (f "/\" L9)))) is M2( the carrier of L)

L is non empty LattStr

the carrier of L is non empty set

L9 is M2( the carrier of L)

f is M2( the carrier of L)

L9 "/\" f is M2( the carrier of L)

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L . (L9,f) is M2( the carrier of L)

(L9 "/\" f) "\/" f is M2( the carrier of L)

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

the L_join of L . ((L9 "/\" f),f) is M2( the carrier of L)

f "/\" L9 is M2( the carrier of L)

the L_meet of L . (f,L9) is M2( the carrier of L)

f "\/" (f "/\" L9) is M2( the carrier of L)

the L_join of L . (f,(f "/\" L9)) is M2( the carrier of L)

f "\/" (L9 "/\" f) is M2( the carrier of L)

the L_join of L . (f,(L9 "/\" f)) is M2( the carrier of L)

L is non empty LattStr

the carrier of L is non empty set

L9 is M2( the carrier of L)

f is M2( the carrier of L)

x is M2( the carrier of L)

f "\/" x is M2( the carrier of L)

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_join of L . (f,x) is M2( the carrier of L)

L9 "\/" (f "\/" x) is M2( the carrier of L)

the L_join of L . (L9,(f "\/" x)) is M2( the carrier of L)

L9 "\/" f is M2( the carrier of L)

the L_join of L . (L9,f) is M2( the carrier of L)

(L9 "\/" f) "\/" x is M2( the carrier of L)

the L_join of L . ((L9 "\/" f),x) is M2( the carrier of L)

x "\/" f is M2( the carrier of L)

the L_join of L . (x,f) is M2( the carrier of L)

L9 "\/" (x "\/" f) is M2( the carrier of L)

the L_join of L . (L9,(x "\/" f)) is M2( the carrier of L)

x "\/" (L9 "\/" f) is M2( the carrier of L)

the L_join of L . (x,(L9 "\/" f)) is M2( the carrier of L)

L9 is M2( the carrier of L)

f is M2( the carrier of L)

x is M2( the carrier of L)

f "/\" x is M2( the carrier of L)

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L . (f,x) is M2( the carrier of L)

L9 "/\" (f "/\" x) is M2( the carrier of L)

the L_meet of L . (L9,(f "/\" x)) is M2( the carrier of L)

L9 "/\" f is M2( the carrier of L)

the L_meet of L . (L9,f) is M2( the carrier of L)

(L9 "/\" f) "/\" x is M2( the carrier of L)

the L_meet of L . ((L9 "/\" f),x) is M2( the carrier of L)

x "/\" f is M2( the carrier of L)

the L_meet of L . (x,f) is M2( the carrier of L)

L9 "/\" (x "/\" f) is M2( the carrier of L)

the L_meet of L . (L9,(x "/\" f)) is M2( the carrier of L)

x "/\" (L9 "/\" f) is M2( the carrier of L)

the L_meet of L . (x,(L9 "/\" f)) is M2( the carrier of L)

L is non empty LattStr

the carrier of L is non empty set

L9 is M2( the carrier of L)

f is M2( the carrier of L)

x is M2( the carrier of L)

f "/\" x is M2( the carrier of L)

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L . (f,x) is M2( the carrier of L)

L9 "/\" (f "/\" x) is M2( the carrier of L)

the L_meet of L . (L9,(f "/\" x)) is M2( the carrier of L)

L9 "/\" x is M2( the carrier of L)

the L_meet of L . (L9,x) is M2( the carrier of L)

f "/\" (L9 "/\" x) is M2( the carrier of L)

the L_meet of L . (f,(L9 "/\" x)) is M2( the carrier of L)

L9 "/\" f is M2( the carrier of L)

the L_meet of L . (L9,f) is M2( the carrier of L)

(L9 "/\" f) "/\" x is M2( the carrier of L)

the L_meet of L . ((L9 "/\" f),x) is M2( the carrier of L)

f "/\" L9 is M2( the carrier of L)

the L_meet of L . (f,L9) is M2( the carrier of L)

(f "/\" L9) "/\" x is M2( the carrier of L)

the L_meet of L . ((f "/\" L9),x) is M2( the carrier of L)

L9 is M2( the carrier of L)

f is M2( the carrier of L)

L9 "/\" f is M2( the carrier of L)

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L . (L9,f) is M2( the carrier of L)

L9 "\/" (L9 "/\" f) is M2( the carrier of L)

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

the L_join of L . (L9,(L9 "/\" f)) is M2( the carrier of L)

f "/\" L9 is M2( the carrier of L)

the L_meet of L . (f,L9) is M2( the carrier of L)

(f "/\" L9) "\/" L9 is M2( the carrier of L)

the L_join of L . ((f "/\" L9),L9) is M2( the carrier of L)

(L9 "/\" f) "\/" L9 is M2( the carrier of L)

the L_join of L . ((L9 "/\" f),L9) is M2( the carrier of L)

L9 is M2( the carrier of L)

f is M2( the carrier of L)

x is M2( the carrier of L)

f "\/" x is M2( the carrier of L)

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_join of L . (f,x) is M2( the carrier of L)

L9 "\/" (f "\/" x) is M2( the carrier of L)

the L_join of L . (L9,(f "\/" x)) is M2( the carrier of L)

L9 "\/" x is M2( the carrier of L)

the L_join of L . (L9,x) is M2( the carrier of L)

f "\/" (L9 "\/" x) is M2( the carrier of L)

the L_join of L . (f,(L9 "\/" x)) is M2( the carrier of L)

L9 "\/" f is M2( the carrier of L)

the L_join of L . (L9,f) is M2( the carrier of L)

(L9 "\/" f) "\/" x is M2( the carrier of L)

the L_join of L . ((L9 "\/" f),x) is M2( the carrier of L)

f "\/" L9 is M2( the carrier of L)

the L_join of L . (f,L9) is M2( the carrier of L)

(f "\/" L9) "\/" x is M2( the carrier of L)

the L_join of L . ((f "\/" L9),x) is M2( the carrier of L)

L is non empty LattStr

L is non empty LattStr

L is non empty reflexive transitive antisymmetric PartialOrdered OrthoRelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is Relation-like set

bool [: the carrier of L, the carrier of L:] is set

the Compl of L is Relation-like V6() non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) M2( bool [: the carrier of L, the carrier of L:])

L9 is Relation-like V6() non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) M2( bool [: the carrier of L, the carrier of L:])

L is non empty Dneg OrthoRelStr

the carrier of L is non empty set

L9 is M2( the carrier of L)

L9 ` is M2( the carrier of L)

(L9 `) ` is M2( the carrier of L)

[: the carrier of L, the carrier of L:] is Relation-like set

bool [: the carrier of L, the carrier of L:] is set

the Compl of L is Relation-like V6() non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) M2( bool [: the carrier of L, the carrier of L:])

f is Relation-like V6() non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) M2( bool [: the carrier of L, the carrier of L:])

f . L9 is M2( the carrier of L)

f . (f . L9) is M2( the carrier of L)

L is non empty reflexive transitive antisymmetric Dneg PartialOrdered OrderInvolutive OrthoRelStr

the carrier of L is non empty set

L9 is M2( the carrier of L)

f is M2( the carrier of L)

f ` is M2( the carrier of L)

L9 ` is M2( the carrier of L)

[: the carrier of L, the carrier of L:] is Relation-like set

bool [: the carrier of L, the carrier of L:] is set

the Compl of L is Relation-like V6() non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) M2( bool [: the carrier of L, the carrier of L:])

x is Relation-like V6() non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) M2( bool [: the carrier of L, the carrier of L:])

x . f is M2( the carrier of L)

x . L9 is M2( the carrier of L)

TrivOrthoRelStr is non empty trivial V50() 1 -element reflexive transitive antisymmetric with_suprema with_infima V168() lower-bounded upper-bounded V174() strict Dneg SubQuasiOrdered QuasiOrdered QuasiPure PartialOrdered Pure OrderInvolutive QuasiOrthocomplemented Orthocomplemented OrthoRelStr

L is non empty \/-SemiLattStr

the carrier of L is non empty set

L is non empty /\-SemiLattStr

the carrier of L is non empty set

L is non empty RelStr

the carrier of L is non empty set

op2 is Relation-like V6() V14([:1,1:]) V18([:1,1:],1) M2( bool [:[:1,1:],1:])

id 1 is Relation-like 1 -defined 1 -valued V6() V7() non empty V14(1) V18(1,1) V19(1) V20(1,1) reflexive symmetric antisymmetric transitive involutive M2( bool [:1,1:])

(1,op2,op2,(id 1)) is () ()

() is ()

the carrier of () is set

L is non empty RelStr

the InternalRel of L is Relation-like M2( bool [: the carrier of L, the carrier of L:])

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is Relation-like set

bool [: the carrier of L, the carrier of L:] is set

field the InternalRel of L is set

the carrier of () is non empty trivial V32() 1 -element set

the InternalRel of () is Relation-like M2( bool [: the carrier of (), the carrier of ():])

[: the carrier of (), the carrier of ():] is Relation-like set

bool [: the carrier of (), the carrier of ():] is set

field the InternalRel of () is set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () () () LattStr

LattRel L is Relation-like set

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is Relation-like set

bool [: the carrier of L, the carrier of L:] is set

{ [b

L9 is set

f is M2( the carrier of L)

x is M2( the carrier of L)

[f,x] is M2( the carrier of [:L,L:])

[:L,L:] is strict LattStr

the carrier of [:L,L:] is set

{f,x} is set

{f} is non empty trivial 1 -element set

{{f,x},{f}} is set

L9 is Relation-like M2( bool [: the carrier of L, the carrier of L:])

f is set

x is set

[f,x] is set

{f,x} is set

{f} is non empty trivial 1 -element set

{{f,x},{f}} is set

[x,f] is set

{x,f} is set

{x} is non empty trivial 1 -element set

{{x,f},{x}} is set

y is M2( the carrier of L)

t is M2( the carrier of L)

f is set

x is set

y is set

[f,x] is set

{f,x} is set

{f} is non empty trivial 1 -element set

{{f,x},{f}} is set

[x,y] is set

{x,y} is set

{x} is non empty trivial 1 -element set

{{x,y},{x}} is set

[f,y] is set

{f,y} is set

{{f,y},{f}} is set

t is M2( the carrier of L)

t is M2( the carrier of L)

xx is M2( the carrier of L)

f is set

[f,f] is set

{f,f} is set

{f} is non empty trivial 1 -element set

{{f,f},{f}} is set

x is M2( the carrier of L)

dom L9 is set

field L9 is set

op1 is Relation-like V6() non empty V14(1) V18(1,1) involutive M2( bool [:1,1:])

(1,op2,op2,(id 1),op1) is () ()

() is ()

TrivOrtLat 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 strict Robbins Huntington join-idempotent well-complemented de_Morgan upper-bounded' lower-bounded' distributive' complemented' () () () OrthoLattStr

the carrier of TrivOrtLat is non empty trivial V32() 1 -element set

L is M2( the carrier of TrivOrtLat)

L ` is M2( the carrier of TrivOrtLat)

(L `) ` is M2( the carrier of TrivOrtLat)

the carrier of TrivOrtLat is non empty trivial V32() 1 -element set

L is M2( the carrier of TrivOrtLat)

L ` is M2( the carrier of TrivOrtLat)

L "\/" (L `) is M2( the carrier of TrivOrtLat)

the L_join of TrivOrtLat is Relation-like V6() V14([: the carrier of TrivOrtLat, the carrier of TrivOrtLat:]) V18([: the carrier of TrivOrtLat, the carrier of TrivOrtLat:], the carrier of TrivOrtLat) M2( bool [:[: the carrier of TrivOrtLat, the carrier of TrivOrtLat:], the carrier of TrivOrtLat:])

[: the carrier of TrivOrtLat, the carrier of TrivOrtLat:] is Relation-like set

[:[: the carrier of TrivOrtLat, the carrier of TrivOrtLat:], the carrier of TrivOrtLat:] is Relation-like set

bool [:[: the carrier of TrivOrtLat, the carrier of TrivOrtLat:], the carrier of TrivOrtLat:] is set

the L_join of TrivOrtLat . (L,(L `)) is M2( the carrier of TrivOrtLat)

L9 is M2( the carrier of TrivOrtLat)

L9 ` is M2( the carrier of TrivOrtLat)

L9 "\/" (L9 `) is M2( the carrier of TrivOrtLat)

the L_join of TrivOrtLat . (L9,(L9 `)) is M2( the carrier of TrivOrtLat)

the carrier of () is set

the carrier of () is non empty trivial V32() 1 -element set

L is M2( the carrier of ())

[L,L] is M2( the carrier of [:(),():])

[:(),():] is strict LattStr

the carrier of [:(),():] is set

{L,L} is set

{L} is non empty trivial 1 -element set

{{L,L},{L}} is set

id {{}} is Relation-like {{}} -defined {{}} -valued V6() V7() non empty V14({{}}) V18({{}},{{}}) V19({{}}) V20({{}},{{}}) reflexive symmetric antisymmetric transitive involutive M2( bool [:{{}},{{}}:])

[:{{}},{{}}:] is Relation-like set

bool [:{{}},{{}}:] is set

the carrier of () is non empty trivial V32() 1 -element set

L9 is M2( the carrier of ())

L9 ` is M2( the carrier of ())

(L9 `) ` is M2( the carrier of ())

the carrier of () is non empty trivial V32() 1 -element set

L9 is M2( the carrier of ())

L9 ` is M2( the carrier of ())

L9 "\/" (L9 `) is M2( the carrier of ())

the L_join of () is Relation-like V6() V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) M2( bool [:[: the carrier of (), the carrier of ():], the carrier of ():])

[: the carrier of (), the carrier of ():] is Relation-like set

[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like set

bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set

the L_join of () . (L9,(L9 `)) is M2( the carrier of ())

f is M2( the carrier of ())

f ` is M2( the carrier of ())

f "\/" (f `) is M2( the carrier of ())

the L_join of () . (f,(f `)) is M2( the carrier of ())

L is non empty LattStr

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( 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

L9 is non empty LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

f is M2( the carrier of L9)

x is M2( the carrier of L9)

f "\/" x is M2( the carrier of L9)

the L_join of L9 . (f,x) is M2( the carrier of L9)

x "\/" f is M2( the carrier of L9)

the L_join of L9 . (x,f) is M2( the carrier of L9)

y is M2( the carrier of L)

t is M2( the carrier of L)

y "\/" t is M2( the carrier of L)

the L_join of L . (y,t) is M2( the carrier of L)

t "\/" y is M2( the carrier of L)

the L_join of L . (t,y) is M2( the carrier of L)

L is non empty LattStr

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( 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

L9 is non empty LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

f is M2( the carrier of L9)

x is M2( the carrier of L9)

f "/\" x is M2( the carrier of L9)

the L_meet of L9 . (f,x) is M2( the carrier of L9)

x "/\" f is M2( the carrier of L9)

the L_meet of L9 . (x,f) is M2( the carrier of L9)

y is M2( the carrier of L)

t is M2( the carrier of L)

y "/\" t is M2( the carrier of L)

the L_meet of L . (y,t) is M2( the carrier of L)

t "/\" y is M2( the carrier of L)

the L_meet of L . (t,y) is M2( the carrier of L)

L is non empty LattStr

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( 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

L9 is non empty LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

f is M2( the carrier of L9)

x is M2( the carrier of L9)

y is M2( the carrier of L9)

x "\/" y is M2( the carrier of L9)

the L_join of L9 . (x,y) is M2( the carrier of L9)

f "\/" (x "\/" y) is M2( the carrier of L9)

the L_join of L9 . (f,(x "\/" y)) is M2( the carrier of L9)

f "\/" x is M2( the carrier of L9)

the L_join of L9 . (f,x) is M2( the carrier of L9)

(f "\/" x) "\/" y is M2( the carrier of L9)

the L_join of L9 . ((f "\/" x),y) is M2( the carrier of L9)

t is M2( the carrier of L)

t is M2( the carrier of L)

t "\/" t is M2( the carrier of L)

the L_join of L . (t,t) is M2( the carrier of L)

xx is M2( the carrier of L)

(t "\/" t) "\/" xx is M2( the carrier of L)

the L_join of L . ((t "\/" t),xx) is M2( the carrier of L)

t "\/" xx is M2( the carrier of L)

the L_join of L . (t,xx) is M2( the carrier of L)

t "\/" (t "\/" xx) is M2( the carrier of L)

the L_join of L . (t,(t "\/" xx)) is M2( the carrier of L)

L is non empty LattStr

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( 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

L9 is non empty LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

f is M2( the carrier of L9)

x is M2( the carrier of L9)

y is M2( the carrier of L9)

x "/\" y is M2( the carrier of L9)

the L_meet of L9 . (x,y) is M2( the carrier of L9)

f "/\" (x "/\" y) is M2( the carrier of L9)

the L_meet of L9 . (f,(x "/\" y)) is M2( the carrier of L9)

f "/\" x is M2( the carrier of L9)

the L_meet of L9 . (f,x) is M2( the carrier of L9)

(f "/\" x) "/\" y is M2( the carrier of L9)

the L_meet of L9 . ((f "/\" x),y) is M2( the carrier of L9)

t is M2( the carrier of L)

t is M2( the carrier of L)

t "/\" t is M2( the carrier of L)

the L_meet of L . (t,t) is M2( the carrier of L)

xx is M2( the carrier of L)

(t "/\" t) "/\" xx is M2( the carrier of L)

the L_meet of L . ((t "/\" t),xx) is M2( the carrier of L)

t "/\" xx is M2( the carrier of L)

the L_meet of L . (t,xx) is M2( the carrier of L)

t "/\" (t "/\" xx) is M2( the carrier of L)

the L_meet of L . (t,(t "/\" xx)) is M2( the carrier of L)

L is non empty LattStr

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( 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

L9 is non empty LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

f is M2( the carrier of L9)

x is M2( the carrier of L9)

f "\/" x is M2( the carrier of L9)

the L_join of L9 . (f,x) is M2( the carrier of L9)

f "/\" (f "\/" x) is M2( the carrier of L9)

the L_meet of L9 . (f,(f "\/" x)) is M2( the carrier of L9)

y is M2( the carrier of L)

t is M2( the carrier of L)

y "\/" t is M2( the carrier of L)

the L_join of L . (y,t) is M2( the carrier of L)

y "/\" (y "\/" t) is M2( the carrier of L)

the L_meet of L . (y,(y "\/" t)) is M2( the carrier of L)

L is non empty LattStr

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( 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

L9 is non empty LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

f is M2( the carrier of L9)

x is M2( the carrier of L9)

f "/\" x is M2( the carrier of L9)

the L_meet of L9 . (f,x) is M2( the carrier of L9)

(f "/\" x) "\/" x is M2( the carrier of L9)

the L_join of L9 . ((f "/\" x),x) is M2( the carrier of L9)

y is M2( the carrier of L)

t is M2( the carrier of L)

y "/\" t is M2( the carrier of L)

the L_meet of L . (y,t) is M2( the carrier of L)

(y "/\" t) "\/" t is M2( the carrier of L)

the L_join of L . ((y "/\" t),t) is M2( the carrier of L)

L is non empty LattStr

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( 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

L9 is non empty LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

L is non empty \/-SemiLattStr

the carrier of L is non empty set

L9 is non empty \/-SemiLattStr

the carrier of L9 is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

\/-SemiLattStr(# the carrier of L, the L_join of L #) is non empty strict \/-SemiLattStr

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

\/-SemiLattStr(# the carrier of L9, the L_join of L9 #) is non empty strict \/-SemiLattStr

f is M2( the carrier of L)

y is M2( the carrier of L9)

x is M2( the carrier of L)

t is M2( the carrier of L9)

f "\/" x is M2( the carrier of L)

the L_join of L . (f,x) is M2( the carrier of L)

y "\/" t is M2( the carrier of L9)

the L_join of L9 . (y,t) is M2( the carrier of L9)

L is non empty /\-SemiLattStr

the carrier of L is non empty set

L9 is non empty /\-SemiLattStr

the carrier of L9 is non empty set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

/\-SemiLattStr(# the carrier of L, the L_meet of L #) is non empty strict /\-SemiLattStr

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

/\-SemiLattStr(# the carrier of L9, the L_meet of L9 #) is non empty strict /\-SemiLattStr

f is M2( the carrier of L)

y is M2( the carrier of L9)

x is M2( the carrier of L)

t is M2( the carrier of L9)

f "/\" x is M2( the carrier of L)

the L_meet of L . (f,x) is M2( the carrier of L)

y "/\" t is M2( the carrier of L9)

the L_meet of L9 . (y,t) is M2( the carrier of L9)

L is non empty ComplStr

the carrier of L is non empty set

L9 is non empty ComplStr

the carrier of L9 is non empty set

the Compl of L is Relation-like V6() non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) M2( bool [: the carrier of L, the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

bool [: the carrier of L, the carrier of L:] is set

the Compl of L9 is Relation-like V6() non empty V14( the carrier of L9) V18( the carrier of L9, the carrier of L9) M2( bool [: the carrier of L9, the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

bool [: the carrier of L9, the carrier of L9:] is set

f is M2( the carrier of L)

f ` is M2( the carrier of L)

x is M2( the carrier of L9)

x ` is M2( the carrier of L9)

the Compl of L9 . x is M2( the carrier of L9)

L is non empty ComplLLattStr

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the Compl of L is Relation-like V6() non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) M2( bool [: the carrier of L, the carrier of L:])

bool [: the carrier of L, the carrier of L:] is set

ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) is strict ComplLLattStr

L9 is non empty ComplLLattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the Compl of L9 is Relation-like V6() non empty V14( the carrier of L9) V18( the carrier of L9, the carrier of L9) M2( bool [: the carrier of L9, the carrier of L9:])

bool [: the carrier of L9, the carrier of L9:] is set

ComplLLattStr(# the carrier of L9, the L_join of L9, the Compl of L9 #) is strict ComplLLattStr

f is M2( the carrier of L9)

f ` is M2( the carrier of L9)

f "\/" (f `) is M2( the carrier of L9)

the L_join of L9 . (f,(f `)) is M2( the carrier of L9)

x is M2( the carrier of L9)

x ` is M2( the carrier of L9)

x "\/" (x `) is M2( the carrier of L9)

the L_join of L9 . (x,(x `)) is M2( the carrier of L9)

y is M2( the carrier of L)

y ` is M2( the carrier of L)

y "\/" (y `) is M2( the carrier of L)

the L_join of L . (y,(y `)) is M2( the carrier of L)

t is M2( the carrier of L)

t ` is M2( the carrier of L)

t "\/" (t `) is M2( the carrier of L)

the L_join of L . (t,(t `)) is M2( the carrier of L)

L is non empty OrthoLattStr

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

the Compl of L is Relation-like V6() non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) M2( bool [: the carrier of L, the carrier of L:])

bool [: the carrier of L, the carrier of L:] is set

OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) is strict OrthoLattStr

L9 is non empty OrthoLattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

the Compl of L9 is Relation-like V6() non empty V14( the carrier of L9) V18( the carrier of L9, the carrier of L9) M2( bool [: the carrier of L9, the carrier of L9:])

bool [: the carrier of L9, the carrier of L9:] is set

OrthoLattStr(# the carrier of L9, the L_join of L9, the L_meet of L9, the Compl of L9 #) is strict OrthoLattStr

f is M2( the carrier of L9)

x is M2( the carrier of L9)

f "/\" x is M2( the carrier of L9)

the L_meet of L9 . (f,x) is M2( the carrier of L9)

f ` is M2( the carrier of L9)

x ` is M2( the carrier of L9)

(f `) "\/" (x `) is M2( the carrier of L9)

the L_join of L9 . ((f `),(x `)) is M2( the carrier of L9)

((f `) "\/" (x `)) ` is M2( the carrier of L9)

y is M2( the carrier of L)

y ` is M2( the carrier of L)

t is M2( the carrier of L)

t ` is M2( the carrier of L)

y "/\" t is M2( the carrier of L)

the L_meet of L . (y,t) is M2( the carrier of L)

(y `) "\/" (t `) is M2( the carrier of L)

the L_join of L . ((y `),(t `)) is M2( the carrier of L)

((y `) "\/" (t `)) ` is M2( the carrier of L)

L is non empty OrthoLattStr

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

the Compl of L is Relation-like V6() non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) M2( bool [: the carrier of L, the carrier of L:])

bool [: the carrier of L, the carrier of L:] is set

OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) is strict OrthoLattStr

L9 is non empty OrthoLattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

the Compl of L9 is Relation-like V6() non empty V14( the carrier of L9) V18( the carrier of L9, the carrier of L9) M2( bool [: the carrier of L9, the carrier of L9:])

bool [: the carrier of L9, the carrier of L9:] is set

OrthoLattStr(# the carrier of L9, the L_join of L9, the L_meet of L9, the Compl of L9 #) is strict OrthoLattStr

f is M2( the carrier of L9)

f ` is M2( the carrier of L9)

(f `) ` is M2( the carrier of L9)

x is M2( the carrier of L)

x ` is M2( the carrier of L)

(x `) ` is M2( the carrier of L)

L is RelStr

the carrier of L is set

the InternalRel of L is Relation-like M2( bool [: the carrier of L, the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

bool [: the carrier of L, the carrier of L:] is set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]) is Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L) is () ()

the carrier of ( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L) is set

the InternalRel of ( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L) is Relation-like M2( bool [: the carrier of ( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L), the carrier of ( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L):])

[: the carrier of ( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L), the carrier of ( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L):] is Relation-like set

bool [: the carrier of ( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L), the carrier of ( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L):] is set

RelStr(# the carrier of ( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L), the InternalRel of ( the carrier of L, the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:]), the InternalRel of L) #) is strict RelStr

L is LattStr

the carrier of L is set

the L_join of L is Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is strict LattStr

bool [: the carrier of L, the carrier of L:] is set

the Relation-like M2( bool [: the carrier of L, the carrier of L:]) is Relation-like M2( bool [: the carrier of L, the carrier of L:])

( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])) is () ()

the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])) is set

the L_join of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])) is Relation-like V6() V18([: the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])), the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:]))) M2( bool [:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])), the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):])

[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])), the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):] is Relation-like set

[:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])), the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):] is Relation-like set

bool [:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])), the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):] is set

the L_meet of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])) is Relation-like V6() V18([: the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])), the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:]))) M2( bool [:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])), the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])):])

LattStr(# the carrier of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])), the L_join of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])), the L_meet of ( the carrier of L, the L_join of L, the L_meet of L, the Relation-like M2( bool [: the carrier of L, the carrier of L:])) #) is strict LattStr

L is non empty LattStr

L9 is (L)

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

the carrier of L9 is set

the L_join of L9 is Relation-like V6() V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

LattStr(# the carrier of L9, the L_join of L9, the L_meet of L9 #) is strict LattStr

L is non empty meet-associative LattStr

L9 is non empty (L)

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

L is non empty join-associative LattStr

L9 is non empty (L)

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

L is non empty meet-commutative LattStr

L9 is non empty (L)

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

L is non empty join-commutative LattStr

L9 is non empty (L)

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:])

[: the carrier of L9, the carrier of L9:] is Relation-like set

[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is Relation-like set

bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is set

the L_meet of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of L9) M2( 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 LattStr

L is non empty join-absorbing LattStr

L9 is non empty (L)

the carrier of L is non empty set

the L_join of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

[: the carrier of L, the carrier of L:] is Relation-like set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set

the L_meet of L is Relation-like V6() V14([: the carrier of L, the carrier of L:]) V18([: the carrier of L, the carrier of L:], the carrier of L) M2( bool [:[: the carrier of L, the carrier of L:], the carrier of L:])

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

the carrier of L9 is non empty set

the L_join of L9 is Relation-like V6() V14([: the carrier of L9, the carrier of L9:]) V18([: the carrier of L9, the carrier of L9:], the carrier of