:: 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<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is M2( the carrier of L) : b<sub>1</sub> [= b<sub>2</sub> } is set
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