:: 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 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-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 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 join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () () () LattStr
(L) is Relation-like V14( the carrier of L) V18( the carrier of L, the carrier of L) reflexive antisymmetric transitive 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
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:], 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 carrier of L, the L_join of L, the L_meet of L,(L)) is () ()
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr
the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)) is set
the L_join of ( the carrier of L, the L_join of L, the L_meet of L,(L)) is Relation-like V6() V18([: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L))) M2( bool [:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):])
[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):] is Relation-like set
[:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):] is Relation-like set
bool [:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):] is set
the L_meet of ( the carrier of L, the L_join of L, the L_meet of L,(L)) is Relation-like V6() V18([: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L))) M2( bool [:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)):])
LattStr(# the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L)), the L_join of ( the carrier of L, the L_join of L, the L_meet of L,(L)), the L_meet of ( the carrier of L, the L_join of L, the L_meet of L,(L)) #) is strict LattStr
x is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () () () (L)
the carrier of x is non empty set
y is M2( the carrier of x)
t is M2( the carrier of x)
y "/\" t is M2( the carrier of x)
the L_meet of x is Relation-like V6() V14([: the carrier of x, the carrier of x:]) V18([: the carrier of x, the carrier of x:], the carrier of x) M2( bool [:[: the carrier of x, the carrier of x:], the carrier of x:])
[: the carrier of x, the carrier of x:] is Relation-like set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the L_meet of x . (y,t) is M2( the carrier of x)
[y,t] is M2( the carrier of [:x,x:])
[:x,x:] is strict LattStr
the carrier of [:x,x:] is set
{y,t} is set
{y} is non empty trivial 1 -element set
{{y,t},{y}} is set
the InternalRel of x is Relation-like M2( bool [: the carrier of x, the carrier of x:])
bool [: the carrier of x, the carrier of x:] is set
t is M2( the carrier of L)
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,xx] is M2( the carrier of [:L,L:])
[:L,L:] is strict LattStr
the carrier of [:L,L:] is set
{t,xx} is set
{t} is non empty trivial 1 -element set
{{t,xx},{t}} is set
y is M2( the carrier of x)
t is M2( the carrier of x)
y "\/" t is M2( the carrier of x)
the L_join of x is Relation-like V6() V14([: the carrier of x, the carrier of x:]) V18([: the carrier of x, the carrier of x:], the carrier of x) M2( bool [:[: the carrier of x, the carrier of x:], the carrier of x:])
[: the carrier of x, the carrier of x:] is Relation-like set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the L_join of x . (y,t) is M2( the carrier of x)
[y,t] is M2( the carrier of [:x,x:])
[:x,x:] is strict LattStr
the carrier of [:x,x:] is set
{y,t} is set
{y} is non empty trivial 1 -element set
{{y,t},{y}} is set
the InternalRel of x is Relation-like M2( bool [: the carrier of x, the carrier of x:])
bool [: the carrier of x, the carrier of x:] is set
t is M2( the carrier of L)
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,xx] is M2( the carrier of [:L,L:])
[:L,L:] is strict LattStr
the carrier of [:L,L:] is set
{t,xx} is set
{t} is non empty trivial 1 -element set
{{t,xx},{t}} is set
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 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 upper-bounded' lower-bounded' distributive' complemented' () () () OrthoLattStr
L9 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 upper-bounded' lower-bounded' distributive' complemented' () () () OrthoLattStr
the carrier of L9 is non empty trivial V32() 1 -element set
f is M2( the carrier of L9)
f ` is M2( the carrier of L9)
(f `) ` is M2( the carrier of L9)
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 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_join of L9 . ((f `),f) is M2( the carrier of L9)
Top L9 is M2( the carrier of L9)
(f `) "/\" f is M2( the carrier of L9)
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 L_meet of L9 . ((f `),f) is M2( the carrier of L9)
Bottom L9 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)
f "/\" (f `) is M2( the carrier of L9)
the L_meet of L9 . (f,(f `)) is M2( the carrier of L9)
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 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_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 L9)
t is M2( the carrier of L9)
y "/\" t is M2( the carrier of L9)
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 L_meet of L9 . (y,t) is M2( the carrier of L9)
y ` is M2( the carrier of L9)
t ` is M2( the carrier of L9)
(y `) "\/" (t `) is M2( the carrier of L9)
the L_join of L9 . ((y `),(t `)) is M2( the carrier of L9)
((y `) "\/" (t `)) ` is M2( the carrier of L9)
L is non empty trivial V50() 1 -element reflexive transitive antisymmetric with_suprema with_infima V168() lower-bounded upper-bounded V174() PartialOrdered OrthoRelStr
L9 is non empty trivial V50() 1 -element reflexive transitive antisymmetric with_suprema with_infima V168() lower-bounded upper-bounded V174() PartialOrdered OrthoRelStr
the carrier of L9 is non empty trivial V32() 1 -element set
[: the carrier of L9, the carrier of L9:] is Relation-like set
bool [: 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:])
x is set
{x} is non empty trivial 1 -element set
f 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:])
id {x} is Relation-like {x} -defined {x} -valued V6() V7() non empty V14({x}) V18({x},{x}) V19({x}) V20({x},{x}) reflexive symmetric antisymmetric transitive involutive M2( bool [:{x},{x}:])
[:{x},{x}:] is Relation-like set
bool [:{x},{x}:] is set
y is M2( the carrier of L9)
t is M2( the carrier of L9)
f . t is M2( the carrier of L9)
f . y is M2( the carrier of L9)
L is non empty trivial V50() 1 -element reflexive transitive antisymmetric join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean with_suprema with_infima V168() lower-bounded upper-bounded V174() upper-bounded' lower-bounded' distributive' complemented' () () () ()
L9 is non empty trivial V50() 1 -element reflexive transitive antisymmetric join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean with_suprema with_infima V168() lower-bounded upper-bounded V174() upper-bounded' lower-bounded' distributive' complemented' () () () ()
the carrier of L9 is non empty trivial V32() 1 -element set
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 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_join of L9 . (f,x) is M2( the carrier of L9)
y is M2( the carrier of L9)
t is M2( the carrier of L9)
y "\/" t is M2( the carrier of L9)
the L_join of L9 . (y,t) is M2( the carrier of L9)
t is M2( the carrier of L9)
xx is M2( the carrier of L9)
t "/\" xx is M2( the carrier of L9)
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 L_meet of L9 . (t,xx) is M2( the carrier of L9)
t is M2( the carrier of L9)
t is M2( the carrier of L9)
t "/\" t is M2( the carrier of L9)
the L_meet of L9 . (t,t) is M2( the carrier of L9)
L is non empty () ()
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_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)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () () () () ()
the carrier of L is non empty 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
LattPOSet L is strict reflexive transitive antisymmetric with_suprema with_infima RelStr
(L) is Relation-like V14( the carrier of L) V18( the carrier of L, the carrier of L) reflexive antisymmetric transitive M2( bool [: the carrier of L, the carrier of L:])
L9 is set
f is set
[L9,f] is set
{L9,f} is set
{L9} is non empty trivial 1 -element set
{{L9,f},{L9}} is set
x is M2( the carrier of L)
y is M2( the carrier of L)
x is M2( the carrier of L)
y is M2( the carrier of L)
RelStr(# the carrier of L,(L) #) is strict RelStr
L is non empty ()
L9 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () () () () ()
LattPOSet L9 is strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L9 is non empty set
the InternalRel of L9 is Relation-like 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
RelStr(# the carrier of L9, the InternalRel of L9 #) is strict RelStr
L is OrthoLattStr
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:])
the Compl of L is Relation-like V6() 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
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:]), the Compl 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:]), the Compl 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:]), the Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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:]), the Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl 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 Compl of L):])
the Compl 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 Compl of L) is Relation-like V6() V14( 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 Compl of L)) 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 Compl 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 Compl 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 Compl 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 Compl of L):])
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 Compl 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 Compl of L):] is set
OrthoLattStr(# 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 Compl 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 Compl 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:]), the Compl of L), the Compl 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 Compl of L) #) is strict OrthoLattStr
L is non empty OrthoLattStr
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:])
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
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:])
the Compl of L9 is Relation-like V6() 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
L is non empty meet-associative OrthoLattStr
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:])
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
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
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr
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 OrthoLattStr
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:])
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
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
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr
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 OrthoLattStr
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:])
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
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
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr
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 OrthoLattStr
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:])
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
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
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr
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-absorbing OrthoLattStr
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:])
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
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
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr
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 OrthoLattStr
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:])
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
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
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr
LattStr(# the carrier of L9, the L_join of L9, the L_meet of L9 #) is non empty strict LattStr
L is non empty () OrthoLattStr
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:])
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
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
ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) is strict ComplLLattStr
ComplLLattStr(# the carrier of L9, the L_join of L9, the Compl of L9 #) is strict ComplLLattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan () () () () () OrthoLattStr
(L) is Relation-like V14( the carrier of L) V18( the carrier of L, the carrier of L) reflexive antisymmetric transitive 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
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:], 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:])
( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L) is () ()
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) is strict OrthoLattStr
the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L) is set
the L_join of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L) is Relation-like V6() V18([: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L)) M2( bool [:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):])
[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):] is Relation-like set
[:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):] is Relation-like set
bool [:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):] is set
the L_meet of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L) is Relation-like V6() V18([: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L)) M2( bool [:[: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):], the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):])
the Compl of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L) is Relation-like V6() V14( the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L)) V18( the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L)) M2( bool [: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):])
bool [: the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L):] is set
OrthoLattStr(# the carrier of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the L_join of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the L_meet of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L), the Compl of ( the carrier of L, the L_join of L, the L_meet of L,(L), the Compl of L) #) is strict OrthoLattStr
x is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () () () () (L)
the carrier of x is non empty set
y is M2( the carrier of x)
t is M2( the carrier of x)
y "/\" t is M2( the carrier of x)
the L_meet of x is Relation-like V6() V14([: the carrier of x, the carrier of x:]) V18([: the carrier of x, the carrier of x:], the carrier of x) M2( bool [:[: the carrier of x, the carrier of x:], the carrier of x:])
[: the carrier of x, the carrier of x:] is Relation-like set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the L_meet of x . (y,t) is M2( the carrier of x)
t is M2( the carrier of L)
xx is M2( the carrier of L)
[t,xx] is M2( the carrier of [:L,L:])
[:L,L:] is strict LattStr
the carrier of [:L,L:] is set
{t,xx} is set
{t} is non empty trivial 1 -element set
{{t,xx},{t}} is set
the InternalRel of x is Relation-like M2( bool [: the carrier of x, the carrier of x:])
bool [: the carrier of x, the carrier of x:] is set
t "/\" xx is M2( the carrier of L)
the L_meet of L . (t,xx) is M2( the carrier of L)
y is M2( the carrier of x)
t is M2( the carrier of x)
y "\/" t is M2( the carrier of x)
the L_join of x is Relation-like V6() V14([: the carrier of x, the carrier of x:]) V18([: the carrier of x, the carrier of x:], the carrier of x) M2( bool [:[: the carrier of x, the carrier of x:], the carrier of x:])
[: the carrier of x, the carrier of x:] is Relation-like set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the L_join of x . (y,t) is M2( the carrier of x)
[y,t] is M2( the carrier of [:x,x:])
[:x,x:] is strict LattStr
the carrier of [:x,x:] is set
{y,t} is set
{y} is non empty trivial 1 -element set
{{y,t},{y}} is set
the InternalRel of x is Relation-like M2( bool [: the carrier of x, the carrier of x:])
bool [: the carrier of x, the carrier of x:] is set
t is M2( the carrier of L)
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,xx] is M2( the carrier of [:L,L:])
[:L,L:] is strict LattStr
the carrier of [:L,L:] is set
{t,xx} is set
{t} is non empty trivial 1 -element set
{{t,xx},{t}} is set
L is non empty reflexive transitive antisymmetric with_suprema with_infima PartialOrdered OrthoRelStr
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)
L9 "/\" f is M2( the carrier of L)
f "\/" L9 is M2( the carrier of L)
L is non empty meet-commutative /\-SemiLattStr
the carrier of L is non empty set
x is M2( the carrier of L)
y is M2( the carrier of L)
x "/\" y 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 . (x,y) is M2( the carrier of L)
y "/\" x is M2( the carrier of L)
the L_meet of L . (y,x) is M2( the carrier of L)
L is non empty join-commutative \/-SemiLattStr
the carrier of L is non empty set
x is M2( the carrier of L)
y is M2( the carrier of L)
x "\/" y 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 . (x,y) is M2( the carrier of L)
y "\/" x is M2( the carrier of L)
the L_join of L . (y,x) is M2( the carrier of L)
L is non empty ()
L9 is non empty meet-commutative meet-absorbing join-absorbing () ()
the carrier of L9 is non empty set
f is M2( the carrier of L9)
L is non empty ()
L9 is non empty join-associative () ()
the carrier of L9 is non empty set
f is M2( the carrier of L9)
x is M2( the carrier of L9)
y is M2( the carrier of L9)
L is non empty ()
L9 is non empty join-commutative () ()
the carrier of L9 is non empty set
f is M2( the carrier of L9)
x is M2( the carrier of L9)
L is non empty reflexive transitive antisymmetric join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like with_suprema with_infima PartialOrdered () () () () ()
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)
(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)
(L,L9,f) "\/" (L9 "\/" f) is M2( the carrier of L)
(L,L9,f) "\/" L9 is M2( the carrier of L)
((L,L9,f) "\/" L9) "\/" f is M2( the carrier of L)
(L,L9,f) "\/" f is M2( the carrier of L)
(L,(L9 "\/" f),(L,L9,f)) is M2( the carrier of L)
the L_join of L . ((L9 "\/" f),(L,L9,f)) is M2( the carrier of L)
(L,(L9 "\/" f),L9) is M2( the carrier of L)
the L_join of L . ((L9 "\/" f),L9) is M2( the carrier of L)
(L,(L,(L9 "\/" f),L9),f) is M2( the carrier of L)
the L_join of L . ((L,(L9 "\/" f),L9),f) is M2( the carrier of L)
(L,(L9 "\/" f),f) is M2( the carrier of L)
the L_join of L . ((L9 "\/" f),f) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like with_suprema with_infima PartialOrdered () () () () ()
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)
(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)
(L,L9,f) "/\" (L9 "/\" f) is M2( the carrier of L)
(L,L9,f) "/\" L9 is M2( the carrier of L)
((L,L9,f) "/\" L9) "/\" f is M2( the carrier of L)
(L,L9,f) "/\" f is M2( the carrier of L)
(L,(L9 "/\" f),(L,L9,f)) is M2( the carrier of L)
the L_meet of L . ((L9 "/\" f),(L,L9,f)) is M2( the carrier of L)
(L,(L9 "/\" f),L9) is M2( the carrier of L)
the L_meet of L . ((L9 "/\" f),L9) is M2( the carrier of L)
(L,(L,(L9 "/\" f),L9),f) is M2( the carrier of L)
the L_meet of L . ((L,(L9 "/\" f),L9),f) is M2( the carrier of L)
(L,(L9 "/\" f),f) is M2( the carrier of L)
the L_meet of L . ((L9 "/\" f),f) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like with_suprema with_infima Dneg PartialOrdered OrderInvolutive () () () () () ()
the carrier of L is non empty set
L9 is M2( the carrier of L)
L9 ` is M2( the carrier of L)
f is M2( the carrier of L)
f ` is M2( the carrier of L)
(L9 `) "\/" (f `) is M2( the carrier of L)
L9 "/\" f is M2( the carrier of L)
(L9 "/\" f) ` is M2( the carrier of L)
((L9 "/\" f) `) "\/" (f `) is M2( the carrier of L)
(f `) "\/" ((L9 "/\" f) `) 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)
(L9 "\/" f) ` 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)
((L9 "\/" f) `) "/\" (f `) is M2( the carrier of L)
L9 is M2( the carrier of L)
L9 ` is M2( the carrier of L)
f is M2( the carrier of L)
f ` is M2( the carrier of L)
(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)
(L,(L9 `),(f `)) ` is M2( the carrier of L)
(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 L_meet of L . (L9,f) is M2( the carrier of L)
(L9 `) "\/" (f `) is M2( the carrier of L)
L9 "/\" f 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)
(L9 "/\" f) ` is M2( the carrier of L)
((L9 "/\" f) `) ` is M2( the carrier of L)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan () () () () () OrthoLattStr
L9 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () () () () (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:])
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
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
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan () () () () () OrthoLattStr
L9 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () () () () () (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:])
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
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
L is non empty ()
L9 is non empty reflexive transitive antisymmetric join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like with_suprema with_infima de_Morgan PartialOrdered () () () () () () ()
the carrier of L9 is non empty set
[: the carrier of L9, the carrier of L9:] is Relation-like set
bool [: 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:])
f 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:])
x is M2( the carrier of L9)
y is M2( the carrier of L9)
f . y is M2( the carrier of L9)
f . x is M2( the carrier of L9)
x ` is M2( the carrier of L9)
(L9,x,y) is M2( the carrier of L9)
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:], 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 . (x,y) is M2( the carrier of L9)
(L9,x,y) ` is M2( the carrier of L9)
y ` is M2( the carrier of L9)
(L9,(x `),(y `)) is M2( the carrier of L9)
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 L_join of L9 . ((x `),(y `)) is M2( the carrier of L9)
(L9,(x `),(y `)) ` is M2( the carrier of L9)
((L9,(x `),(y `)) `) ` is M2( the carrier of L9)
"\/" ( the carrier of L9,L9) is M2( the carrier of L9)
y is M2( the carrier of L9)
f . y is M2( the carrier of L9)
{y,(f . y)} is set
"\/" ({y,(f . y)},L9) is M2( the carrier of L9)
"/\" ({y,(f . y)},L9) is M2( the carrier of L9)
y ` is M2( the carrier of L9)
(L9,y,(y `)) is M2( the carrier of L9)
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:], 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_join of L9 . (y,(y `)) is M2( the carrier of L9)
t is M2( the carrier of L9)
(L9,t,(L9,y,(y `))) is M2( the carrier of L9)
the L_join of L9 . (t,(L9,y,(y `))) is M2( the carrier of L9)
t ` is M2( the carrier of L9)
(L9,t,(t `)) is M2( the carrier of L9)
the L_join of L9 . (t,(t `)) is M2( the carrier of L9)
(L9,t,(L9,t,(t `))) is M2( the carrier of L9)
the L_join of L9 . (t,(L9,t,(t `))) is M2( the carrier of L9)
(L9,t,t) is M2( the carrier of L9)
the L_join of L9 . (t,t) is M2( the carrier of L9)
(L9,(L9,t,t),(t `)) is M2( the carrier of L9)
the L_join of L9 . ((L9,t,t),(t `)) is M2( the carrier of L9)
t is M2( the carrier of L9)
xx is M2( the carrier of L9)
{y,(y `)} is set
"\/" ({y,(y `)},L9) is M2( the carrier of L9)
y "\/" (y `) is M2( the carrier of L9)
"/\" ( the carrier of L9,L9) is M2( the carrier of L9)
(L9,y,(y `)) is M2( the carrier of L9)
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 L_meet of L9 . (y,(y `)) is M2( the carrier of L9)
t is M2( the carrier of L9)
t ` is M2( the carrier of L9)
(L9,t,(t `)) is M2( the carrier of L9)
the L_meet of L9 . (t,(t `)) is M2( the carrier of L9)
b is M2( the carrier of L9)
b ` is M2( the carrier of L9)
(L9,b,(b `)) is M2( the carrier of L9)
the L_meet of L9 . (b,(b `)) is M2( the carrier of L9)
(t `) ` is M2( the carrier of L9)
(L9,(t `),((t `) `)) is M2( the carrier of L9)
the L_join of L9 . ((t `),((t `) `)) is M2( the carrier of L9)
(L9,(t `),((t `) `)) ` is M2( the carrier of L9)
(b `) ` is M2( the carrier of L9)
(L9,(b `),((b `) `)) is M2( the carrier of L9)
the L_join of L9 . ((b `),((b `) `)) is M2( the carrier of L9)
(L9,(b `),((b `) `)) ` is M2( the carrier of L9)
t is M2( the carrier of L9)
(L9,t,(L9,y,(y `))) is M2( the carrier of L9)
the L_meet of L9 . (t,(L9,y,(y `))) is M2( the carrier of L9)
t ` is M2( the carrier of L9)
(L9,t,(t `)) is M2( the carrier of L9)
the L_meet of L9 . (t,(t `)) is M2( the carrier of L9)
(L9,t,(L9,t,(t `))) is M2( the carrier of L9)
the L_meet of L9 . (t,(L9,t,(t `))) is M2( the carrier of L9)
(L9,t,t) is M2( the carrier of L9)
the L_meet of L9 . (t,t) is M2( the carrier of L9)
(L9,(L9,t,t),(t `)) is M2( the carrier of L9)
the L_meet of L9 . ((L9,t,t),(t `)) is M2( the carrier of L9)
t is M2( the carrier of L9)
b is M2( the carrier of L9)
"/\" ({y,(y `)},L9) is M2( the carrier of L9)
y "/\" (y `) is M2( the carrier of L9)
x is M2( the carrier of L9)
f . x is M2( the carrier of L9)
f . (f . x) is M2( the carrier of L9)
x ` is M2( the carrier of L9)
f . (x `) is M2( the carrier of L9)
(x `) ` is M2( the carrier of L9)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan () () () () () OrthoLattStr
L9 is non empty reflexive transitive antisymmetric join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like with_suprema with_infima de_Morgan PartialOrdered () () () () () () (L)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan () () () () () OrthoLattStr
L9 is non empty reflexive transitive antisymmetric join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like with_suprema with_infima de_Morgan PartialOrdered () () () () () () (L)
L is non empty OrthoLattStr
L9 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean Robbins Huntington join-idempotent well-complemented upper-bounded' lower-bounded' distributive' complemented' () () () OrthoLattStr
the carrier of L9 is non empty set
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 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 . (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 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 L_join of L9 . ((f `),(x `)) is M2( the carrier of L9)
((f `) "\/" (x `)) ` is M2( the carrier of L9)
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 L9)
x ` is M2( the carrier of L9)
(L9,x,(x `)) is M2( the carrier of L9)
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_join of L9 . (x,(x `)) is M2( the carrier of L9)
y is M2( the carrier of L9)
y ` is M2( the carrier of L9)
(L9,y,(y `)) is M2( the carrier of L9)
the L_join of L9 . (y,(y `)) is M2( the carrier of L9)
L is non empty OrthoLattStr