REAL is non empty V36() V37() V38() V42() V59() set
NAT is V36() V37() V38() V39() V40() V41() V42() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V36() V42() V59() set
ExtREAL is non empty V37() set
omega is V36() V37() V38() V39() V40() V41() V42() set
bool omega is non empty set
[:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty set
bool [:[:REAL,REAL:],REAL:] is non empty set
bool NAT is non empty set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is non empty set
Nat_Lattice is non empty strict LattStr
the carrier of Nat_Lattice is non empty set
NATPLUS is V36() V37() V38() V39() V40() V41() Element of bool NAT
[:NATPLUS,NATPLUS:] is set
[:[:NATPLUS,NATPLUS:],NATPLUS:] is set
bool [:[:NATPLUS,NATPLUS:],NATPLUS:] is non empty set
{} is empty V36() V37() V38() V39() V40() V41() V42() set
the empty V36() V37() V38() V39() V40() V41() V42() set is empty V36() V37() V38() V39() V40() V41() V42() set
1 is non empty natural V31() V32() ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT
minreal is V1() V4([:REAL,REAL:]) V5( REAL ) Function-like V18([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
maxreal is V1() V4([:REAL,REAL:]) V5( REAL ) Function-like V18([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
Real_Lattice is strict LattStr
LattStr(# REAL,maxreal,minreal #) is non empty strict LattStr
the carrier of Real_Lattice is set
0 is empty natural V31() V32() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() Element of NAT
+infty is non empty V32() ext-real positive non negative set
{+infty} is non empty V37() set
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
id c2 is V1() V4(L) Function-like V14(L) ManySortedFunction of c2,c2
A is set
(id c2) . A is set
c2 . A is set
[:(c2 . A),(c2 . A):] is set
bool [:(c2 . A),(c2 . A):] is non empty set
id (c2 . A) is V1() V4(c2 . A) V5(c2 . A) V14(c2 . A) Element of bool [:(c2 . A),(c2 . A):]
A is V1() V4(L) Function-like V14(L) ManySortedRelation of c2,c2
B is set
c2 . B is set
[:(c2 . B),(c2 . B):] is set
bool [:(c2 . B),(c2 . B):] is non empty set
A . B is set
Ma is V1() V4(c2 . B) V5(c2 . B) Element of bool [:(c2 . B),(c2 . B):]
id (c2 . B) is V1() V4(c2 . B) V5(c2 . B) V14(c2 . B) Element of bool [:(c2 . B),(c2 . B):]
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
[|c2,c2|] is V1() V4(L) Function-like V14(L) set
A is set
[|c2,c2|] . A is set
c2 . A is set
[:(c2 . A),(c2 . A):] is set
bool [:(c2 . A),(c2 . A):] is non empty set
A is V1() V4(L) Function-like V14(L) ManySortedRelation of c2,c2
B is set
c2 . B is set
[:(c2 . B),(c2 . B):] is set
bool [:(c2 . B),(c2 . B):] is non empty set
A . B is set
Ma is V1() V4(c2 . B) V5(c2 . B) Element of bool [:(c2 . B),(c2 . B):]
nabla (c2 . B) is V1() V4(c2 . B) V5(c2 . B) Element of bool [:(c2 . B),(c2 . B):]
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
EqRelLatt c2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (EqRelLatt c2) is non empty set
[|c2,c2|] is V1() V4(L) Function-like V14(L) set
R is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
A is Element of the carrier of (EqRelLatt c2)
B is Element of the carrier of (EqRelLatt c2)
A "\/" B is Element of the carrier of (EqRelLatt c2)
B "\/" A is Element of the carrier of (EqRelLatt c2)
Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
R \/ Ma is V1() V4(L) Function-like V14(L) set
R "\/" Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Mi is set
c2 . Mi is set
[:(c2 . Mi),(c2 . Mi):] is set
bool [:(c2 . Mi),(c2 . Mi):] is non empty set
Ma is Element of L
R . Ma is V1() V4(c2 . Ma) V5(c2 . Ma) Element of bool [:(c2 . Ma),(c2 . Ma):]
c2 . Ma is set
[:(c2 . Ma),(c2 . Ma):] is set
bool [:(c2 . Ma),(c2 . Ma):] is non empty set
Ma . Ma is V1() V4(c2 . Ma) V5(c2 . Ma) Element of bool [:(c2 . Ma),(c2 . Ma):]
(R \/ Ma) . Mi is set
R . Mi is set
Ma . Mi is set
(R . Mi) \/ (Ma . Mi) is set
[:(c2 . Mi),(c2 . Mi):] \/ (Ma . Mi) is set
nabla (c2 . Mi) is V1() V4(c2 . Mi) V5(c2 . Mi) Element of bool [:(c2 . Mi),(c2 . Mi):]
ma is V1() V4(c2 . Mi) V5(c2 . Mi) V14(c2 . Mi) V114() V119() Element of bool [:(c2 . Mi),(c2 . Mi):]
(nabla (c2 . Mi)) \/ ma is V1() V4(c2 . Mi) V5(c2 . Mi) Element of bool [:(c2 . Mi),(c2 . Mi):]
(R "\/" Ma) . Mi is set
Mi is V1() V4(c2 . Mi) V5(c2 . Mi) V14(c2 . Mi) V114() V119() Element of bool [:(c2 . Mi),(c2 . Mi):]
EqCl Mi is V1() V4(c2 . Mi) V5(c2 . Mi) V14(c2 . Mi) V114() V119() Element of bool [:(c2 . Mi),(c2 . Mi):]
mi is V1() V4(L) Function-like V14(L) ManySortedRelation of c2,c2
EqCl mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
the L_join of (EqRelLatt c2) is V1() V4([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):]) V5( the carrier of (EqRelLatt c2)) Function-like V18([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2)) Element of bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):]
[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):] is non empty set
[:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
the L_join of (EqRelLatt c2) . (A,B) is Element of the carrier of (EqRelLatt c2)
[A,B] is set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
the L_join of (EqRelLatt c2) . [A,B] is set
R is Element of the carrier of (EqRelLatt c2)
id c2 is V1() V4(L) Function-like V14(L) ManySortedFunction of c2,c2
R is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
A is Element of the carrier of (EqRelLatt c2)
B is Element of the carrier of (EqRelLatt c2)
A "/\" B is Element of the carrier of (EqRelLatt c2)
B "/\" A is Element of the carrier of (EqRelLatt c2)
Mi is set
c2 . Mi is set
[:(c2 . Mi),(c2 . Mi):] is set
bool [:(c2 . Mi),(c2 . Mi):] is non empty set
Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Ma is Element of L
Ma . Ma is V1() V4(c2 . Ma) V5(c2 . Ma) Element of bool [:(c2 . Ma),(c2 . Ma):]
c2 . Ma is set
[:(c2 . Ma),(c2 . Ma):] is set
bool [:(c2 . Ma),(c2 . Ma):] is non empty set
R /\ Ma is V1() V4(L) Function-like V14(L) set
(R /\ Ma) . Mi is set
R . Mi is set
Ma . Mi is set
(R . Mi) /\ (Ma . Mi) is set
id (c2 . Mi) is V1() V4(c2 . Mi) V5(c2 . Mi) V14(c2 . Mi) Element of bool [:(c2 . Mi),(c2 . Mi):]
Mi is V1() V4(c2 . Mi) V5(c2 . Mi) V14(c2 . Mi) V114() V119() Element of bool [:(c2 . Mi),(c2 . Mi):]
(id (c2 . Mi)) /\ Mi is V1() V4(c2 . Mi) V5(c2 . Mi) Element of bool [:(c2 . Mi),(c2 . Mi):]
the L_meet of (EqRelLatt c2) is V1() V4([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):]) V5( the carrier of (EqRelLatt c2)) Function-like V18([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2)) Element of bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):]
[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):] is non empty set
[:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
the L_meet of (EqRelLatt c2) . (A,B) is Element of the carrier of (EqRelLatt c2)
[A,B] is set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
the L_meet of (EqRelLatt c2) . [A,B] is set
R is Element of the carrier of (EqRelLatt c2)
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
EqRelLatt c2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Bottom (EqRelLatt c2) is Element of the carrier of (EqRelLatt c2)
the carrier of (EqRelLatt c2) is non empty set
id c2 is V1() V4(L) Function-like V14(L) ManySortedFunction of c2,c2
A is Element of the carrier of (EqRelLatt c2)
B is Element of the carrier of (EqRelLatt c2)
Ma is set
c2 . Ma is set
[:(c2 . Ma),(c2 . Ma):] is set
bool [:(c2 . Ma),(c2 . Ma):] is non empty set
Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Mi is Element of L
Mi . Mi is V1() V4(c2 . Mi) V5(c2 . Mi) Element of bool [:(c2 . Mi),(c2 . Mi):]
c2 . Mi is set
[:(c2 . Mi),(c2 . Mi):] is set
bool [:(c2 . Mi),(c2 . Mi):] is non empty set
Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Ma /\ Mi is V1() V4(L) Function-like V14(L) set
(Ma /\ Mi) . Ma is set
Ma . Ma is set
Mi . Ma is set
(Ma . Ma) /\ (Mi . Ma) is set
id (c2 . Ma) is V1() V4(c2 . Ma) V5(c2 . Ma) V14(c2 . Ma) Element of bool [:(c2 . Ma),(c2 . Ma):]
ma is V1() V4(c2 . Ma) V5(c2 . Ma) V14(c2 . Ma) V114() V119() Element of bool [:(c2 . Ma),(c2 . Ma):]
(id (c2 . Ma)) /\ ma is V1() V4(c2 . Ma) V5(c2 . Ma) Element of bool [:(c2 . Ma),(c2 . Ma):]
A "/\" B is Element of the carrier of (EqRelLatt c2)
the L_meet of (EqRelLatt c2) is V1() V4([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):]) V5( the carrier of (EqRelLatt c2)) Function-like V18([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2)) Element of bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):]
[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):] is non empty set
[:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
the L_meet of (EqRelLatt c2) . (A,B) is Element of the carrier of (EqRelLatt c2)
[A,B] is set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
the L_meet of (EqRelLatt c2) . [A,B] is set
B "/\" A is Element of the carrier of (EqRelLatt c2)
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
EqRelLatt c2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Top (EqRelLatt c2) is Element of the carrier of (EqRelLatt c2)
the carrier of (EqRelLatt c2) is non empty set
[|c2,c2|] is V1() V4(L) Function-like V14(L) set
A is Element of the carrier of (EqRelLatt c2)
B is Element of the carrier of (EqRelLatt c2)
Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Ma \/ Mi is V1() V4(L) Function-like V14(L) set
Ma "\/" Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Ma is set
c2 . Ma is set
[:(c2 . Ma),(c2 . Ma):] is set
bool [:(c2 . Ma),(c2 . Ma):] is non empty set
Mi is Element of L
Ma . Mi is V1() V4(c2 . Mi) V5(c2 . Mi) Element of bool [:(c2 . Mi),(c2 . Mi):]
c2 . Mi is set
[:(c2 . Mi),(c2 . Mi):] is set
bool [:(c2 . Mi),(c2 . Mi):] is non empty set
Mi . Mi is V1() V4(c2 . Mi) V5(c2 . Mi) Element of bool [:(c2 . Mi),(c2 . Mi):]
(Ma \/ Mi) . Ma is set
Ma . Ma is set
Mi . Ma is set
(Ma . Ma) \/ (Mi . Ma) is set
[:(c2 . Ma),(c2 . Ma):] \/ (Mi . Ma) is set
nabla (c2 . Ma) is V1() V4(c2 . Ma) V5(c2 . Ma) Element of bool [:(c2 . Ma),(c2 . Ma):]
mi is V1() V4(c2 . Ma) V5(c2 . Ma) V14(c2 . Ma) V114() V119() Element of bool [:(c2 . Ma),(c2 . Ma):]
(nabla (c2 . Ma)) \/ mi is V1() V4(c2 . Ma) V5(c2 . Ma) Element of bool [:(c2 . Ma),(c2 . Ma):]
(Ma "\/" Mi) . Ma is set
ma is V1() V4(c2 . Ma) V5(c2 . Ma) V14(c2 . Ma) V114() V119() Element of bool [:(c2 . Ma),(c2 . Ma):]
EqCl ma is V1() V4(c2 . Ma) V5(c2 . Ma) V14(c2 . Ma) V114() V119() Element of bool [:(c2 . Ma),(c2 . Ma):]
L is V1() V4(L) Function-like V14(L) ManySortedRelation of c2,c2
EqCl L is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
A "\/" B is Element of the carrier of (EqRelLatt c2)
the L_join of (EqRelLatt c2) is V1() V4([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):]) V5( the carrier of (EqRelLatt c2)) Function-like V18([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2)) Element of bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):]
[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):] is non empty set
[:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
the L_join of (EqRelLatt c2) . (A,B) is Element of the carrier of (EqRelLatt c2)
[A,B] is set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
the L_join of (EqRelLatt c2) . [A,B] is set
B "\/" A is Element of the carrier of (EqRelLatt c2)
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
EqRelLatt c2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
the carrier of (EqRelLatt c2) is non empty set
bool the carrier of (EqRelLatt c2) is non empty set
[|c2,c2|] is V1() V4(L) Function-like V14(L) set
Bool [|c2,c2|] is functional non empty V145() set
bool (Bool [|c2,c2|]) is non empty set
R is Element of bool the carrier of (EqRelLatt c2)
A is set
Ma is set
Mi is Element of L
c2 . Mi is set
B is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
B . Mi is V1() V4(c2 . Mi) V5(c2 . Mi) Element of bool [:(c2 . Mi),(c2 . Mi):]
[:(c2 . Mi),(c2 . Mi):] is set
bool [:(c2 . Mi),(c2 . Mi):] is non empty set
B . Ma is set
[|c2,c2|] . Ma is set
Bool [|c2,c2|] is functional non empty V145() additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool [|c2,c2|])
bool the carrier of (EqRelLatt c2) is non empty Element of bool (bool the carrier of (EqRelLatt c2))
bool (bool the carrier of (EqRelLatt c2)) is non empty set
bool (Bool [|c2,c2|]) is non empty Element of bool (bool (Bool [|c2,c2|]))
bool (Bool [|c2,c2|]) is non empty set
bool (bool (Bool [|c2,c2|])) is non empty set
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
EqRelLatt c2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
the carrier of (EqRelLatt c2) is non empty set
R is Element of the carrier of (EqRelLatt c2)
A is Element of the carrier of (EqRelLatt c2)
B is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
B /\ Ma is V1() V4(L) Function-like V14(L) set
the L_meet of (EqRelLatt c2) is V1() V4([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):]) V5( the carrier of (EqRelLatt c2)) Function-like V18([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2)) Element of bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):]
[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):] is non empty set
[:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
the L_meet of (EqRelLatt c2) . (B,Ma) is set
[B,Ma] is set
{B,Ma} is non empty set
{B} is non empty set
{{B,Ma},{B}} is non empty set
the L_meet of (EqRelLatt c2) . [B,Ma] is set
R "/\" A is Element of the carrier of (EqRelLatt c2)
R "/\" A is Element of the carrier of (EqRelLatt c2)
the L_meet of (EqRelLatt c2) is V1() V4([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):]) V5( the carrier of (EqRelLatt c2)) Function-like V18([: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2)) Element of bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):]
[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):] is non empty set
[:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
bool [:[: the carrier of (EqRelLatt c2), the carrier of (EqRelLatt c2):], the carrier of (EqRelLatt c2):] is non empty set
the L_meet of (EqRelLatt c2) . (B,Ma) is set
[B,Ma] is set
{B,Ma} is non empty set
{B} is non empty set
{{B,Ma},{B}} is non empty set
the L_meet of (EqRelLatt c2) . [B,Ma] is set
B /\ Ma is V1() V4(L) Function-like V14(L) set
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
EqRelLatt c2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
the carrier of (EqRelLatt c2) is non empty set
bool the carrier of (EqRelLatt c2) is non empty set
[|c2,c2|] is V1() V4(L) Function-like V14(L) set
Bool [|c2,c2|] is functional non empty V145() set
bool (Bool [|c2,c2|]) is non empty set
R is Element of bool the carrier of (EqRelLatt c2)
A is Element of bool (Bool [|c2,c2|])
|:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c2,c2|])
K200(L,[|c2,c2|]) is V1() V4(L) Function-like V14(L) set
meet |:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of [|c2,c2|]
B is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Bool [|c2,c2|] is functional non empty V145() additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool [|c2,c2|])
Ma is set
|:A:| . Ma is set
{ (b1 . Ma) where b1 is V1() V4(L) Function-like V14(L) Element of Bool [|c2,c2|] : b1 in A } is set
Mi is V1() V4(L) Function-like V14(L) Element of Bool [|c2,c2|]
Mi . Ma is set
meet (|:A:| . Ma) is set
Ma . Ma is set
Mi is set
[|c2,c2|] . Ma is set
bool ([|c2,c2|] . Ma) is non empty set
bool (bool ([|c2,c2|] . Ma)) is non empty set
(meet |:A:|) . Ma is set
B . Ma is set
Mi is Element of bool (bool ([|c2,c2|] . Ma))
Intersect Mi is Element of bool ([|c2,c2|] . Ma)
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
EqRelLatt c2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
the carrier of (EqRelLatt c2) is non empty set
bool the carrier of (EqRelLatt c2) is non empty set
[|c2,c2|] is V1() V4(L) Function-like V14(L) set
Bool [|c2,c2|] is functional non empty V145() set
bool (Bool [|c2,c2|]) is non empty set
R is Element of bool the carrier of (EqRelLatt c2)
A is Element of bool (Bool [|c2,c2|])
|:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c2,c2|])
K200(L,[|c2,c2|]) is V1() V4(L) Function-like V14(L) set
meet |:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of [|c2,c2|]
Ma is set
(meet |:A:|) . Ma is set
[|c2,c2|] . Ma is set
c2 . Ma is set
[:(c2 . Ma),(c2 . Ma):] is set
bool [:(c2 . Ma),(c2 . Ma):] is non empty set
Ma is set
c2 . Ma is set
[:(c2 . Ma),(c2 . Ma):] is set
bool [:(c2 . Ma),(c2 . Ma):] is non empty set
Ma is V1() V4(L) Function-like V14(L) ManySortedRelation of c2,c2
Ma . Ma is set
Mi is V1() V4(c2 . Ma) V5(c2 . Ma) Element of bool [:(c2 . Ma),(c2 . Ma):]
bool (bool [:(c2 . Ma),(c2 . Ma):]) is non empty set
ma is Element of L
|:A:| . ma is Element of bool (bool ([|c2,c2|] . ma))
[|c2,c2|] . ma is set
bool ([|c2,c2|] . ma) is non empty set
bool (bool ([|c2,c2|] . ma)) is non empty set
[|c2,c2|] . Ma is set
bool ([|c2,c2|] . Ma) is non empty set
bool (bool ([|c2,c2|] . Ma)) is non empty set
|:A:| . Ma is set
L is Element of bool (bool ([|c2,c2|] . Ma))
Intersect L is Element of bool ([|c2,c2|] . Ma)
Mi is non empty Element of bool (Bool [|c2,c2|])
|:Mi:| is V1() non-empty V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c2,c2|])
mi is Element of bool (bool [:(c2 . Ma),(c2 . Ma):])
|:Mi:| . Ma is set
Bool [|c2,c2|] is functional non empty V145() additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool [|c2,c2|])
{ (b1 . Ma) where b1 is V1() V4(L) Function-like V14(L) Element of Bool [|c2,c2|] : b1 in A } is set
ma is set
mi is Element of bool (bool [:(c2 . Ma),(c2 . Ma):])
L9 is V1() V4(L) Function-like V14(L) Element of Bool [|c2,c2|]
L9 . Ma is set
L9 is V1() V4(c2 . Ma) V5(c2 . Ma) Element of bool [:(c2 . Ma),(c2 . Ma):]
meet mi is V1() V4(c2 . Ma) V5(c2 . Ma) Element of bool [:(c2 . Ma),(c2 . Ma):]
L is non empty LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
c2 is Element of bool the carrier of L
c2 is set
{ b1 where b1 is Element of the carrier of L : S1[b1] } is set
A is Element of the carrier of L
B is Element of the carrier of L
B is Element of the carrier of L
Ma is Element of the carrier of L
Mi is Element of the carrier of L
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
EqRelLatt c2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
the carrier of (EqRelLatt c2) is non empty set
bool the carrier of (EqRelLatt c2) is non empty set
R is Element of bool the carrier of (EqRelLatt c2)
[|c2,c2|] is V1() V4(L) Function-like V14(L) set
Bool [|c2,c2|] is functional non empty V145() set
bool (Bool [|c2,c2|]) is non empty set
Top (EqRelLatt c2) is Element of the carrier of (EqRelLatt c2)
B is Element of the carrier of (EqRelLatt c2)
Ma is Element of the carrier of (EqRelLatt c2)
Ma is Element of the carrier of (EqRelLatt c2)
A is Element of bool (Bool [|c2,c2|])
|:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c2,c2|])
K200(L,[|c2,c2|]) is V1() V4(L) Function-like V14(L) set
meet |:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of [|c2,c2|]
B is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Mi is Element of the carrier of (EqRelLatt c2)
Ma is Element of the carrier of (EqRelLatt c2)
Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Ma is Element of the carrier of (EqRelLatt c2)
mi is set
[|c2,c2|] . mi is set
bool ([|c2,c2|] . mi) is non empty set
bool (bool ([|c2,c2|] . mi)) is non empty set
|:A:| . mi is set
(meet |:A:|) . mi is set
ma is non empty Element of bool (Bool [|c2,c2|])
|:ma:| is V1() non-empty V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c2,c2|])
L is set
|:ma:| . mi is set
Bool [|c2,c2|] is functional non empty V145() additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool [|c2,c2|])
{ (b1 . mi) where b1 is V1() V4(L) Function-like V14(L) Element of Bool [|c2,c2|] : b1 in A } is set
mi is V1() V4(L) Function-like V14(L) Element of Bool [|c2,c2|]
mi . mi is set
ma is Element of the carrier of (EqRelLatt c2)
Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
L9 is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Mi . mi is set
meet (|:A:| . mi) is set
L is Element of bool (bool ([|c2,c2|] . mi))
Intersect L is Element of bool ([|c2,c2|] . mi)
Ma is Element of the carrier of (EqRelLatt c2)
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
EqRelLatt c2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
L is non empty set
c2 is V1() V4(L) Function-like V14(L) set
EqRelLatt c2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt c2) is non empty set
bool the carrier of (EqRelLatt c2) is non empty set
[|c2,c2|] is V1() V4(L) Function-like V14(L) set
Bool [|c2,c2|] is functional non empty V145() set
bool (Bool [|c2,c2|]) is non empty set
R is Element of bool the carrier of (EqRelLatt c2)
"/\" (R,(EqRelLatt c2)) is Element of the carrier of (EqRelLatt c2)
{ b1 where b1 is Element of the carrier of (EqRelLatt c2) : b1 is_less_than R } is set
"\/" ( { b1 where b1 is Element of the carrier of (EqRelLatt c2) : b1 is_less_than R } ,(EqRelLatt c2)) is Element of the carrier of (EqRelLatt c2)
A is Element of bool (Bool [|c2,c2|])
|:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c2,c2|])
K200(L,[|c2,c2|]) is V1() V4(L) Function-like V14(L) set
meet |:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of [|c2,c2|]
B is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
Mi is Element of the carrier of (EqRelLatt c2)
Ma is non empty Element of bool (Bool [|c2,c2|])
|:Ma:| is V1() non-empty V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c2,c2|])
L is V1() V4(L) Function-like V14(L) set
mi is V1() non-empty V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c2,c2|])
mi is set
L . mi is set
|:A:| . mi is set
|:Ma:| . mi is set
Bool [|c2,c2|] is functional non empty V145() additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool [|c2,c2|])
{ (b1 . mi) where b1 is V1() V4(L) Function-like V14(L) Element of Bool [|c2,c2|] : b1 in A } is set
ma is V1() V4(L) Function-like V14(L) Element of Bool [|c2,c2|]
ma . mi is set
L9 is Element of the carrier of (EqRelLatt c2)
ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
L9 is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
ma . mi is set
Mi is Element of the carrier of (EqRelLatt c2)
Ma is Element of the carrier of (EqRelLatt c2)
Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c2,c2
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
the carrier of c2 is non empty set
R is Element of the carrier of L
A is Element of the carrier of L
R "\/" A is Element of the carrier of L
R "/\" A is Element of the carrier of L
B is Element of the carrier of c2
Ma is Element of the carrier of c2
B "\/" Ma is Element of the carrier of c2
B "/\" Ma is Element of the carrier of c2
the L_join of L is V1() V4([: the carrier of L, the carrier of L:]) V5( the carrier of L) Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (R,A) is Element of the carrier of L
[R,A] is set
{R,A} is non empty set
{R} is non empty set
{{R,A},{R}} is non empty set
the L_join of L . [R,A] is set
the L_join of L || the carrier of c2 is V1() Function-like set
[: the carrier of c2, the carrier of c2:] is non empty set
K5( the L_join of L,[: the carrier of c2, the carrier of c2:]) is V1() set
[B,Ma] is Element of [: the carrier of c2, the carrier of c2:]
{B,Ma} is non empty set
{B} is non empty set
{{B,Ma},{B}} is non empty set
( the L_join of L || the carrier of c2) . [B,Ma] is set
the L_join of c2 is V1() V4([: the carrier of c2, the carrier of c2:]) V5( the carrier of c2) Function-like V18([: the carrier of c2, the carrier of c2:], the carrier of c2) Element of bool [:[: the carrier of c2, the carrier of c2:], the carrier of c2:]
[:[: the carrier of c2, the carrier of c2:], the carrier of c2:] is non empty set
bool [:[: the carrier of c2, the carrier of c2:], the carrier of c2:] is non empty set
the L_join of c2 . (B,Ma) is Element of the carrier of c2
[B,Ma] is set
the L_join of c2 . [B,Ma] is set
the L_meet of L is V1() V4([: the carrier of L, the carrier of L:]) V5( the carrier of L) Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . (R,A) is Element of the carrier of L
the L_meet of L . [R,A] is set
the L_meet of L || the carrier of c2 is V1() Function-like set
K5( the L_meet of L,[: the carrier of c2, the carrier of c2:]) is V1() set
( the L_meet of L || the carrier of c2) . [B,Ma] is set
the L_meet of c2 is V1() V4([: the carrier of c2, the carrier of c2:]) V5( the carrier of c2) Function-like V18([: the carrier of c2, the carrier of c2:], the carrier of c2) Element of bool [:[: the carrier of c2, the carrier of c2:], the carrier of c2:]
the L_meet of c2 . (B,Ma) is Element of the carrier of c2
the L_meet of c2 . [B,Ma] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
the carrier of c2 is non empty set
bool the carrier of c2 is non empty set
R is Element of bool the carrier of c2
A is Element of the carrier of L
B is Element of the carrier of c2
Ma is Element of the carrier of c2
Mi is Element of the carrier of L
B "/\" Ma is Element of the carrier of c2
A "/\" Mi is Element of the carrier of L
Ma is Element of the carrier of L
Mi is Element of the carrier of c2
A "/\" Ma is Element of the carrier of L
B "/\" Mi is Element of the carrier of c2
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
the carrier of c2 is non empty set
bool the carrier of c2 is non empty set
R is Element of bool the carrier of c2
A is Element of the carrier of L
B is Element of the carrier of c2
Ma is Element of the carrier of c2
Mi is Element of the carrier of L
Ma "/\" B is Element of the carrier of c2
Mi "/\" A is Element of the carrier of L
Ma is Element of the carrier of L
Mi is Element of the carrier of c2
Ma "/\" A is Element of the carrier of L
Mi "/\" B is Element of the carrier of c2
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
the carrier of c2 is non empty set
bool the carrier of c2 is non empty set
R is Element of bool the carrier of c2
"/\" (R,L) is Element of the carrier of L
the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : b1 is_less_than R } is set
"\/" ( { b1 where b1 is Element of the carrier of L : b1 is_less_than R } ,L) is Element of the carrier of L
B is Element of the carrier of c2
Ma is Element of the carrier of c2
Mi is Element of the carrier of L
Ma "/\" B is Element of the carrier of c2
Mi "/\" ("/\" (R,L)) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
the carrier of c2 is non empty set
bool the carrier of c2 is non empty set
R is Element of bool the carrier of c2
"\/" (R,L) is Element of the carrier of L
the carrier of L is non empty set
B is Element of the carrier of c2
Ma is Element of the carrier of c2
Mi is Element of the carrier of L
B "/\" Ma is Element of the carrier of c2
("\/" (R,L)) "/\" Mi is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
the carrier of c2 is non empty set
bool the carrier of c2 is non empty set
A is Element of bool the carrier of c2
"/\" (A,L) is Element of the carrier of L
the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : b1 is_less_than A } is set
"\/" ( { b1 where b1 is Element of the carrier of L : b1 is_less_than A } ,L) is Element of the carrier of L
"/\" (A,c2) is Element of the carrier of c2
{ b1 where b1 is Element of the carrier of c2 : b1 is_less_than A } is set
"\/" ( { b1 where b1 is Element of the carrier of c2 : b1 is_less_than A } ,c2) is Element of the carrier of c2
R is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete SubLattice of L
the carrier of R is non empty set
Mi is Element of the carrier of R
Ma is Element of the carrier of L
Ma is Element of the carrier of R
Mi "/\" Ma is Element of the carrier of R
Ma "/\" ("/\" (A,L)) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
the carrier of c2 is non empty set
bool the carrier of c2 is non empty set
A is Element of bool the carrier of c2
"\/" (A,L) is Element of the carrier of L
the carrier of L is non empty set
"\/" (A,c2) is Element of the carrier of c2
R is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete SubLattice of L
the carrier of R is non empty set
Mi is Element of the carrier of R
Ma is Element of the carrier of L
Ma is Element of the carrier of R
Ma "/\" Mi is Element of the carrier of R
("\/" (A,L)) "/\" Ma is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
the carrier of c2 is non empty set
bool the carrier of c2 is non empty set
R is Element of bool the carrier of L
A is Element of bool the carrier of c2
"/\" (R,L) is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_less_than R } is set
"\/" ( { b1 where b1 is Element of the carrier of L : b1 is_less_than R } ,L) is Element of the carrier of L
"/\" (A,c2) is Element of the carrier of c2
{ b1 where b1 is Element of the carrier of c2 : b1 is_less_than A } is set
"\/" ( { b1 where b1 is Element of the carrier of c2 : b1 is_less_than A } ,c2) is Element of the carrier of c2
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L
the carrier of c2 is non empty set
bool the carrier of c2 is non empty set
R is Element of bool the carrier of L
A is Element of bool the carrier of c2
"\/" (R,L) is Element of the carrier of L
"\/" (A,c2) is Element of the carrier of c2
L is V31() V32() ext-real Element of REAL
c2 is V31() V32() ext-real Element of REAL
[.L,c2.] is V36() V37() V38() Element of bool REAL
maxreal || [.L,c2.] is V1() Function-like set
[:[.L,c2.],[.L,c2.]:] is set
K5(maxreal,[:[.L,c2.],[.L,c2.]:]) is V1() set
minreal || [.L,c2.] is V1() Function-like set
K5(minreal,[:[.L,c2.],[.L,c2.]:]) is V1() set
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( L <= b1 & b1 <= c2 ) } is set
R is non empty set
[:R,R:] is non empty set
[:[:R,R:],REAL:] is non empty set
bool [:[:R,R:],REAL:] is non empty set
maxreal || R is V1() Function-like set
K5(maxreal,[:R,R:]) is V1() set
minreal || R is V1() Function-like set
K5(minreal,[:R,R:]) is V1() set
B is V1() V4([:R,R:]) V5( REAL ) Function-like V18([:R,R:], REAL ) Element of bool [:[:R,R:],REAL:]
dom B is V1() V4(R) V5(R) Element of bool [:R,R:]
bool [:R,R:] is non empty set
Ma is set
Mi is set
Ma is set
[Mi,Ma] is set
{Mi,Ma} is non empty set
{Mi} is non empty set
{{Mi,Ma},{Mi}} is non empty set
Mi is V31() V32() ext-real Element of REAL
ma is V31() V32() ext-real Element of REAL
B . Ma is set
minreal . (Mi,Ma) is set
minreal . [Mi,Ma] is set
min (ma,Mi) is V31() V32() ext-real set
Ma is set
A is V1() V4([:R,R:]) V5( REAL ) Function-like V18([:R,R:], REAL ) Element of bool [:[:R,R:],REAL:]
dom A is V1() V4(R) V5(R) Element of bool [:R,R:]
Mi is set
Ma is set
[Mi,Ma] is set
{Mi,Ma} is non empty set
{Mi} is non empty set
{{Mi,Ma},{Mi}} is non empty set
Mi is V31() V32() ext-real Element of REAL
ma is V31() V32() ext-real Element of REAL
A . Ma is set
maxreal . (Mi,Ma) is set
maxreal . [Mi,Ma] is set
max (ma,Mi) is V31() V32() ext-real set
[:[:R,R:],R:] is non empty set
bool [:[:R,R:],R:] is non empty set
Mi is V1() V4([:R,R:]) V5(R) Function-like V18([:R,R:],R) Element of bool [:[:R,R:],R:]
Ma is V1() V4([:R,R:]) V5(R) Function-like V18([:R,R:],R) Element of bool [:[:R,R:],R:]
LattStr(# R,Mi,Ma #) is non empty strict LattStr
ma is non empty LattStr
the carrier of ma is non empty set
mi is Element of the carrier of ma
L is Element of the carrier of ma
mi "\/" L is Element of the carrier of ma
the L_join of ma is V1() V4([: the carrier of ma, the carrier of ma:]) V5( the carrier of ma) Function-like V18([: the carrier of ma, the carrier of ma:], the carrier of ma) Element of bool [:[: the carrier of ma, the carrier of ma:], the carrier of ma:]
[: the carrier of ma, the carrier of ma:] is non empty set
[:[: the carrier of ma, the carrier of ma:], the carrier of ma:] is non empty set
bool [:[: the carrier of ma, the carrier of ma:], the carrier of ma:] is non empty set
the L_join of ma . (mi,L) is Element of the carrier of ma
[mi,L] is set
{mi,L} is non empty set
{mi} is non empty set
{{mi,L},{mi}} is non empty set
the L_join of ma . [mi,L] is set
[mi,L] is Element of [: the carrier of ma, the carrier of ma:]
maxreal . [mi,L] is set
maxreal . (mi,L) is set
maxreal . [mi,L] is set
mi "/\" L is Element of the carrier of ma
the L_meet of ma is V1() V4([: the carrier of ma, the carrier of ma:]) V5( the carrier of ma) Function-like V18([: the carrier of ma, the carrier of ma:], the carrier of ma) Element of bool [:[: the carrier of ma, the carrier of ma:], the carrier of ma:]
the L_meet of ma . (mi,L) is Element of the carrier of ma
the L_meet of ma . [mi,L] is set
minreal . [mi,L] is set
minreal . (mi,L) is set
minreal . [mi,L] is set
mi is Element of R
L is V31() V32() ext-real Element of REAL
mi is Element of the carrier of ma
L is Element of the carrier of ma
mi "\/" L is Element of the carrier of ma
maxreal . (mi,L) is set
[mi,L] is set
{mi,L} is non empty set
{mi} is non empty set
{{mi,L},{mi}} is non empty set
maxreal . [mi,L] is set
ma is Element of the carrier of Real_Lattice
mi is Element of the carrier of Real_Lattice
maxreal . (ma,mi) is set
[ma,mi] is set
{ma,mi} is non empty set
{ma} is non empty set
{{ma,mi},{ma}} is non empty set
maxreal . [ma,mi] is set
L "\/" mi is Element of the carrier of ma
mi is Element of the carrier of ma
L is Element of the carrier of ma
mi "\/" L is Element of the carrier of ma
mi "/\" (mi "\/" L) is Element of the carrier of ma
minreal . (mi,(mi "\/" L)) is set
[mi,(mi "\/" L)] is set
{mi,(mi "\/" L)} is non empty set
{mi} is non empty set
{{mi,(mi "\/" L)},{mi}} is non empty set
minreal . [mi,(mi "\/" L)] is set
mi is Element of the carrier of Real_Lattice
ma is Element of the carrier of Real_Lattice
maxreal . (mi,ma) is set
[mi,ma] is set
{mi,ma} is non empty set
{mi} is non empty set
{{mi,ma},{mi}} is non empty set
maxreal . [mi,ma] is set
minreal . (mi,(maxreal . (mi,ma))) is set
[mi,(maxreal . (mi,ma))] is set
{mi,(maxreal . (mi,ma))} is non empty set
{{mi,(maxreal . (mi,ma))},{mi}} is non empty set
minreal . [mi,(maxreal . (mi,ma))] is set
mi is Element of the carrier of ma
L is Element of the carrier of ma
mi "/\" L is Element of the carrier of ma
minreal . (mi,L) is set
[mi,L] is set
{mi,L} is non empty set
{mi} is non empty set
{{mi,L},{mi}} is non empty set
minreal . [mi,L] is set
ma is Element of the carrier of Real_Lattice
mi is Element of the carrier of Real_Lattice
minreal . (ma,mi) is set
[ma,mi] is set
{ma,mi} is non empty set
{ma} is non empty set
{{ma,mi},{ma}} is non empty set
minreal . [ma,mi] is set
L "/\" mi is Element of the carrier of ma
mi is Element of the carrier of ma
L is Element of the carrier of ma
mi "/\" L is Element of the carrier of ma
(mi "/\" L) "\/" L is Element of the carrier of ma
maxreal . ((mi "/\" L),L) is set
[(mi "/\" L),L] is set
{(mi "/\" L),L} is non empty set
{(mi "/\" L)} is non empty set
{{(mi "/\" L),L},{(mi "/\" L)}} is non empty set
maxreal . [(mi "/\" L),L] is set
mi is Element of the carrier of Real_Lattice
ma is Element of the carrier of Real_Lattice
minreal . (mi,ma) is set
[mi,ma] is set
{mi,ma} is non empty set
{mi} is non empty set
{{mi,ma},{mi}} is non empty set
minreal . [mi,ma] is set
maxreal . ((minreal . (mi,ma)),ma) is set
[(minreal . (mi,ma)),ma] is set
{(minreal . (mi,ma)),ma} is non empty set
{(minreal . (mi,ma))} is non empty set
{{(minreal . (mi,ma)),ma},{(minreal . (mi,ma))}} is non empty set
maxreal . [(minreal . (mi,ma)),ma] is set
mi is Element of the carrier of ma
L is Element of the carrier of ma
mi is Element of the carrier of ma
L "/\" mi is Element of the carrier of ma
mi "/\" (L "/\" mi) is Element of the carrier of ma
minreal . (mi,(L "/\" mi)) is set
[mi,(L "/\" mi)] is set
{mi,(L "/\" mi)} is non empty set
{mi} is non empty set
{{mi,(L "/\" mi)},{mi}} is non empty set
minreal . [mi,(L "/\" mi)] is set
minreal . (L,mi) is set
[L,mi] is set
{L,mi} is non empty set
{L} is non empty set
{{L,mi},{L}} is non empty set
minreal . [L,mi] is set
minreal . (mi,(minreal . (L,mi))) is set
[mi,(minreal . (L,mi))] is set
{mi,(minreal . (L,mi))} is non empty set
{{mi,(minreal . (L,mi))},{mi}} is non empty set
minreal . [mi,(minreal . (L,mi))] is set
ma is Element of the carrier of Real_Lattice
L9 is Element of the carrier of Real_Lattice
minreal . (ma,L9) is set
[ma,L9] is set
{ma,L9} is non empty set
{ma} is non empty set
{{ma,L9},{ma}} is non empty set
minreal . [ma,L9] is set
L9 is Element of the carrier of Real_Lattice
minreal . ((minreal . (ma,L9)),L9) is set
[(minreal . (ma,L9)),L9] is set
{(minreal . (ma,L9)),L9} is non empty set
{(minreal . (ma,L9))} is non empty set
{{(minreal . (ma,L9)),L9},{(minreal . (ma,L9))}} is non empty set
minreal . [(minreal . (ma,L9)),L9] is set
mi "/\" L is Element of the carrier of ma
minreal . ((mi "/\" L),mi) is set
[(mi "/\" L),mi] is set
{(mi "/\" L),mi} is non empty set
{(mi "/\" L)} is non empty set
{{(mi "/\" L),mi},{(mi "/\" L)}} is non empty set
minreal . [(mi "/\" L),mi] is set
(mi "/\" L) "/\" mi is Element of the carrier of ma
mi is Element of the carrier of ma
L is Element of the carrier of ma
mi is Element of the carrier of ma
L "\/" mi is Element of the carrier of ma
mi "\/" (L "\/" mi) is Element of the carrier of ma
maxreal . (mi,(L "\/" mi)) is set
[mi,(L "\/" mi)] is set
{mi,(L "\/" mi)} is non empty set
{mi} is non empty set
{{mi,(L "\/" mi)},{mi}} is non empty set
maxreal . [mi,(L "\/" mi)] is set
maxreal . (L,mi) is set
[L,mi] is set
{L,mi} is non empty set
{L} is non empty set
{{L,mi},{L}} is non empty set
maxreal . [L,mi] is set
maxreal . (mi,(maxreal . (L,mi))) is set
[mi,(maxreal . (L,mi))] is set
{mi,(maxreal . (L,mi))} is non empty set
{{mi,(maxreal . (L,mi))},{mi}} is non empty set
maxreal . [mi,(maxreal . (L,mi))] is set
ma is Element of the carrier of Real_Lattice
L9 is Element of the carrier of Real_Lattice
maxreal . (ma,L9) is set
[ma,L9] is set
{ma,L9} is non empty set
{ma} is non empty set
{{ma,L9},{ma}} is non empty set
maxreal . [ma,L9] is set
L9 is Element of the carrier of Real_Lattice
maxreal . ((maxreal . (ma,L9)),L9) is set
[(maxreal . (ma,L9)),L9] is set
{(maxreal . (ma,L9)),L9} is non empty set
{(maxreal . (ma,L9))} is non empty set
{{(maxreal . (ma,L9)),L9},{(maxreal . (ma,L9))}} is non empty set
maxreal . [(maxreal . (ma,L9)),L9] is set
mi "\/" L is Element of the carrier of ma
maxreal . ((mi "\/" L),mi) is set
[(mi "\/" L),mi] is set
{(mi "\/" L),mi} is non empty set
{(mi "\/" L)} is non empty set
{{(mi "\/" L),mi},{(mi "\/" L)}} is non empty set
maxreal . [(mi "\/" L),mi] is set
(mi "\/" L) "\/" mi is Element of the carrier of ma
mi is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of mi is non empty set
the L_join of mi is V1() V4([: the carrier of mi, the carrier of mi:]) V5( the carrier of mi) Function-like V18([: the carrier of mi, the carrier of mi:], the carrier of mi) Element of bool [:[: the carrier of mi, the carrier of mi:], the carrier of mi:]
[: the carrier of mi, the carrier of mi:] is non empty set
[:[: the carrier of mi, the carrier of mi:], the carrier of mi:] is non empty set
bool [:[: the carrier of mi, the carrier of mi:], the carrier of mi:] is non empty set
the L_meet of mi is V1() V4([: the carrier of mi, the carrier of mi:]) V5( the carrier of mi) Function-like V18([: the carrier of mi, the carrier of mi:], the carrier of mi) Element of bool [:[: the carrier of mi, the carrier of mi:], the carrier of mi:]
R is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of R is non empty set
the L_join of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the L_meet of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of A is non empty set
the L_join of A is V1() V4([: the carrier of A, the carrier of A:]) V5( the carrier of A) Function-like V18([: the carrier of A, the carrier of A:], the carrier of A) Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty set
[:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
the L_meet of A is V1() V4([: the carrier of A, the carrier of A:]) V5( the carrier of A) Function-like V18([: the carrier of A, the carrier of A:], the carrier of A) Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
L is V31() V32() ext-real Element of REAL
c2 is V31() V32() ext-real Element of REAL
(L,c2) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
[.L,c2.] is V36() V37() V38() Element of bool REAL
the carrier of (L,c2) is non empty set
the L_meet of (L,c2) is V1() V4([: the carrier of (L,c2), the carrier of (L,c2):]) V5( the carrier of (L,c2)) Function-like V18([: the carrier of (L,c2), the carrier of (L,c2):], the carrier of (L,c2)) Element of bool [:[: the carrier of (L,c2), the carrier of (L,c2):], the carrier of (L,c2):]
[: the carrier of (L,c2), the carrier of (L,c2):] is non empty set
[:[: the carrier of (L,c2), the carrier of (L,c2):], the carrier of (L,c2):] is non empty set
bool [:[: the carrier of (L,c2), the carrier of (L,c2):], the carrier of (L,c2):] is non empty set
minreal || [.L,c2.] is V1() Function-like set
[:[.L,c2.],[.L,c2.]:] is set
K5(minreal,[:[.L,c2.],[.L,c2.]:]) is V1() set
bool the carrier of (L,c2) is non empty set
Mi is Element of bool the carrier of (L,c2)
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( L <= b1 & b1 <= c2 ) } is set
Ma is Element of the carrier of (L,c2)
Mi is Element of the carrier of (L,c2)
Mi is Element of the carrier of (L,c2)
Mi "/\" Ma is Element of the carrier of (L,c2)
(minreal || [.L,c2.]) . (Mi,Ma) is set
[Mi,Ma] is set
{Mi,Ma} is non empty set
{Mi} is non empty set
{{Mi,Ma},{Mi}} is non empty set
(minreal || [.L,c2.]) . [Mi,Ma] is set
[Mi,Ma] is Element of [: the carrier of (L,c2), the carrier of (L,c2):]
minreal . [Mi,Ma] is set
minreal . (Mi,Ma) is set
minreal . [Mi,Ma] is set
ma is V31() V32() ext-real Element of REAL
min (ma,c2) is V31() V32() ext-real set
mi is V31() V32() ext-real Element of REAL
Mi is Element of bool the carrier of (L,c2)
bool ExtREAL is non empty set
Ma is non empty V37() Element of bool ExtREAL
the ext-real Element of Ma is ext-real Element of Ma
inf Ma is ext-real set
L - 1 is V31() V32() ext-real Element of REAL
L is ext-real set
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( L <= b1 & b1 <= c2 ) } is set
mi is V31() V32() ext-real Element of REAL
L - 0 is V31() V32() ext-real Element of REAL
(L - 1) + L is V31() V32() ext-real Element of REAL
L + mi is V31() V32() ext-real Element of REAL
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( L <= b1 & b1 <= c2 ) } is set
A is ext-real Element of ExtREAL
L is V31() V32() ext-real Element of REAL
L is V31() V32() ext-real Element of REAL
mi is V31() V32() ext-real Element of REAL
ma is ext-real set
R is ext-real Element of ExtREAL
L9 is V31() V32() ext-real Element of REAL
ma is Element of the carrier of (L,c2)
L9 is Element of the carrier of (L,c2)
L9 is V31() V32() ext-real Element of REAL
L9 is V31() V32() ext-real Element of REAL
z is ext-real Element of ExtREAL
ma "/\" L9 is Element of the carrier of (L,c2)
(minreal || [.L,c2.]) . (ma,L9) is set
[ma,L9] is set
{ma,L9} is non empty set
{ma} is non empty set
{{ma,L9},{ma}} is non empty set
(minreal || [.L,c2.]) . [ma,L9] is set
[ma,L9] is Element of [: the carrier of (L,c2), the carrier of (L,c2):]
minreal . [ma,L9] is set
minreal . (ma,L9) is set
minreal . [ma,L9] is set
min (L9,L9) is V31() V32() ext-real set
X is V31() V32() ext-real Element of REAL
X is V31() V32() ext-real Element of REAL
L9 is Element of the carrier of (L,c2)
L9 is V31() V32() ext-real Element of REAL
X is ext-real set
X is Element of the carrier of (L,c2)
X is V31() V32() ext-real Element of REAL
min (L9,X) is V31() V32() ext-real set
minreal . (L9,X) is set
[L9,X] is set
{L9,X} is non empty set
{L9} is non empty set
{{L9,X},{L9}} is non empty set
minreal . [L9,X] is set
[L9,X] is Element of [: the carrier of (L,c2), the carrier of (L,c2):]
(minreal || [.L,c2.]) . [L9,X] is set
(minreal || [.L,c2.]) . (L9,X) is set
(minreal || [.L,c2.]) . [L9,X] is set
L9 "/\" X is Element of the carrier of (L,c2)
z is ext-real Element of ExtREAL
L9 "/\" ma is Element of the carrier of (L,c2)
(minreal || [.L,c2.]) . (L9,ma) is set
[L9,ma] is set
{L9,ma} is non empty set
{{L9,ma},{L9}} is non empty set
(minreal || [.L,c2.]) . [L9,ma] is set
[L9,ma] is Element of [: the carrier of (L,c2), the carrier of (L,c2):]
minreal . [L9,ma] is set
minreal . (L9,ma) is set
minreal . [L9,ma] is set
min (L9,L9) is V31() V32() ext-real set
Mi is Element of bool the carrier of (L,c2)
(0,1) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
{0,1} is non empty V36() V37() V38() V39() V40() V41() Element of bool REAL
2 is non empty natural V31() V32() ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT
1 / 2 is V31() V32() ext-real non negative Element of REAL
].(1 / 2),1.[ is V36() V37() V38() Element of bool REAL
{0,1} \/ ].(1 / 2),1.[ is non empty V36() V37() V38() Element of bool REAL
{0} is non empty V36() V37() V38() V39() V40() V41() Element of bool REAL
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( not b1 <= 1 / 2 & b1 <= 1 ) } is set
{0} \/ { b1 where b1 is V31() V32() ext-real Element of REAL : ( not b1 <= 1 / 2 & b1 <= 1 ) } is non empty set
A is set
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( not b1 <= 1 / 2 & not 1 <= b1 ) } is set
B is V31() V32() ext-real Element of REAL
A is set
B is V31() V32() ext-real Element of REAL
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( not b1 <= 1 / 2 & not 1 <= b1 ) } is set
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
[.0,1.] is V36() V37() V38() Element of bool REAL
the L_meet of (0,1) is V1() V4([: the carrier of (0,1), the carrier of (0,1):]) V5( the carrier of (0,1)) Function-like V18([: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1)) Element of bool [:[: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1):]
the carrier of (0,1) is non empty set
[: the carrier of (0,1), the carrier of (0,1):] is non empty set
[:[: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1):] is non empty set
bool [:[: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1):] is non empty set
minreal || [.0,1.] is V1() Function-like set
[:[.0,1.],[.0,1.]:] is set
K5(minreal,[:[.0,1.],[.0,1.]:]) is V1() set
the L_join of (0,1) is V1() V4([: the carrier of (0,1), the carrier of (0,1):]) V5( the carrier of (0,1)) Function-like V18([: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1)) Element of bool [:[: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1):]
maxreal || [.0,1.] is V1() Function-like set
K5(maxreal,[:[.0,1.],[.0,1.]:]) is V1() set
A is non empty set
[:A,A:] is non empty set
[:[:A,A:],A:] is non empty set
bool [:[:A,A:],A:] is non empty set
maxreal || A is V1() Function-like set
K5(maxreal,[:A,A:]) is V1() set
minreal || A is V1() Function-like set
K5(minreal,[:A,A:]) is V1() set
Ma is set
B is non empty set
Mi is V31() V32() ext-real Element of REAL
[:B,B:] is non empty set
[:[:B,B:],A:] is non empty set
bool [:[:B,B:],A:] is non empty set
Ma is V1() V4([:A,A:]) V5(A) Function-like V18([:A,A:],A) Element of bool [:[:A,A:],A:]
Ma || B is V1() Function-like set
K5(Ma,[:B,B:]) is V1() set
Mi is V1() V4([:A,A:]) V5(A) Function-like V18([:A,A:],A) Element of bool [:[:A,A:],A:]
Mi || B is V1() Function-like set
K5(Mi,[:B,B:]) is V1() set
ma is Element of A
mi is V31() V32() ext-real Element of REAL
Mi is V1() V4([:B,B:]) V5(A) Function-like V18([:B,B:],A) Element of bool [:[:B,B:],A:]
dom Mi is V1() V4(B) V5(B) Element of bool [:B,B:]
bool [:B,B:] is non empty set
ma is set
mi is set
L is set
[mi,L] is set
{mi,L} is non empty set
{mi} is non empty set
{{mi,L},{mi}} is non empty set
Mi . ma is set
Mi . [mi,L] is set
minreal . (mi,L) is set
minreal . [mi,L] is set
min (0,0) is V31() V32() ext-real set
mi is V31() V32() ext-real Element of REAL
Mi . ma is set
Mi . [mi,L] is set
minreal . (mi,L) is set
minreal . [mi,L] is set
min (0,mi) is V31() V32() ext-real set
Mi . ma is set
Mi . ma is set
mi is V31() V32() ext-real Element of REAL
Mi . ma is set
Mi . [mi,L] is set
minreal . (mi,L) is set
minreal . [mi,L] is set
min (mi,0) is V31() V32() ext-real set
ma is V31() V32() ext-real Element of REAL
Mi . ma is set
Mi . [mi,L] is set
minreal . (mi,L) is set
minreal . [mi,L] is set
min (mi,ma) is V31() V32() ext-real set
Mi . ma is set
Mi . ma is set
Mi . ma is set
Mi . ma is set
Ma is V1() V4([:B,B:]) V5(A) Function-like V18([:B,B:],A) Element of bool [:[:B,B:],A:]
dom Ma is V1() V4(B) V5(B) Element of bool [:B,B:]
ma is set
mi is set
L is set
[mi,L] is set
{mi,L} is non empty set
{mi} is non empty set
{{mi,L},{mi}} is non empty set
Ma . ma is set
Ma . [mi,L] is set
maxreal . (mi,L) is set
maxreal . [mi,L] is set
max (0,0) is V31() V32() ext-real set
mi is V31() V32() ext-real Element of REAL
Ma . ma is set
Ma . [mi,L] is set
maxreal . (mi,L) is set
maxreal . [mi,L] is set
max (0,mi) is V31() V32() ext-real set
Ma . ma is set
Ma . ma is set
mi is V31() V32() ext-real Element of REAL
Ma . ma is set
Ma . [mi,L] is set
maxreal . (mi,L) is set
maxreal . [mi,L] is set
max (mi,0) is V31() V32() ext-real set
ma is V31() V32() ext-real Element of REAL
Ma . ma is set
Ma . [mi,L] is set
maxreal . (mi,L) is set
maxreal . [mi,L] is set
max (mi,ma) is V31() V32() ext-real set
Ma . ma is set
Ma . ma is set
Ma . ma is set
Ma . ma is set
[:[:B,B:],B:] is non empty set
bool [:[:B,B:],B:] is non empty set
mi is V1() V4([:B,B:]) V5(B) Function-like V18([:B,B:],B) Element of bool [:[:B,B:],B:]
ma is V1() V4([:B,B:]) V5(B) Function-like V18([:B,B:],B) Element of bool [:[:B,B:],B:]
LattStr(# B,mi,ma #) is non empty strict LattStr
L is non empty LattStr
the carrier of L is non empty set
mi is Element of the carrier of L
ma is Element of the carrier of L
[mi,ma] is Element of [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
{mi,ma} is non empty set
{mi} is non empty set
{{mi,ma},{mi}} is non empty set
mi "\/" ma is Element of the carrier of L
the L_join of L is V1() V4([: the carrier of L, the carrier of L:]) V5( the carrier of L) Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (mi,ma) is Element of the carrier of L
[mi,ma] is set
the L_join of L . [mi,ma] is set
(maxreal || A) . [mi,ma] is set
maxreal . (mi,ma) is set
maxreal . [mi,ma] is set
mi "/\" ma is Element of the carrier of L
the L_meet of L is V1() V4([: the carrier of L, the carrier of L:]) V5( the carrier of L) Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the L_meet of L . (mi,ma) is Element of the carrier of L
the L_meet of L . [mi,ma] is set
(minreal || A) . [mi,ma] is set
minreal . (mi,ma) is set
minreal . [mi,ma] is set
ma is Element of B
mi is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of mi is non empty set
ma is Element of B
L9 is V31() V32() ext-real Element of REAL
mi is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of mi is non empty set
ma is Element of B
mi is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of mi is non empty set
ma is Element of B
mi is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of mi is non empty set
ma is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of mi
L9 is Element of the carrier of mi
ma "\/" L9 is Element of the carrier of L
maxreal . (ma,L9) is set
[ma,L9] is set
{ma,L9} is non empty set
{ma} is non empty set
{{ma,L9},{ma}} is non empty set
maxreal . [ma,L9] is set
X is Element of the carrier of Real_Lattice
z is Element of the carrier of Real_Lattice
maxreal . (X,z) is set
[X,z] is set
{X,z} is non empty set
{X} is non empty set
{{X,z},{X}} is non empty set
maxreal . [X,z] is set
L9 "\/" ma is Element of the carrier of L
ma is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of mi
L9 is Element of the carrier of mi
ma "\/" L9 is Element of the carrier of L
ma "/\" (ma "\/" L9) is Element of the carrier of L
minreal . (ma,(ma "\/" L9)) is set
[ma,(ma "\/" L9)] is set
{ma,(ma "\/" L9)} is non empty set
{ma} is non empty set
{{ma,(ma "\/" L9)},{ma}} is non empty set
minreal . [ma,(ma "\/" L9)] is set
z is Element of the carrier of Real_Lattice
X is Element of the carrier of Real_Lattice
maxreal . (z,X) is set
[z,X] is set
{z,X} is non empty set
{z} is non empty set
{{z,X},{z}} is non empty set
maxreal . [z,X] is set
minreal . (z,(maxreal . (z,X))) is set
[z,(maxreal . (z,X))] is set
{z,(maxreal . (z,X))} is non empty set
{{z,(maxreal . (z,X))},{z}} is non empty set
minreal . [z,(maxreal . (z,X))] is set
ma is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of mi
L9 is Element of the carrier of mi
ma "/\" L9 is Element of the carrier of L
minreal . (ma,L9) is set
[ma,L9] is set
{ma,L9} is non empty set
{ma} is non empty set
{{ma,L9},{ma}} is non empty set
minreal . [ma,L9] is set
X is Element of the carrier of Real_Lattice
z is Element of the carrier of Real_Lattice
minreal . (X,z) is set
[X,z] is set
{X,z} is non empty set
{X} is non empty set
{{X,z},{X}} is non empty set
minreal . [X,z] is set
L9 "/\" ma is Element of the carrier of L
ma is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of mi
L9 is Element of the carrier of mi
ma "/\" L9 is Element of the carrier of L
(ma "/\" L9) "\/" L9 is Element of the carrier of L
maxreal . ((ma "/\" L9),L9) is set
[(ma "/\" L9),L9] is set
{(ma "/\" L9),L9} is non empty set
{(ma "/\" L9)} is non empty set
{{(ma "/\" L9),L9},{(ma "/\" L9)}} is non empty set
maxreal . [(ma "/\" L9),L9] is set
z is Element of the carrier of Real_Lattice
X is Element of the carrier of Real_Lattice
minreal . (z,X) is set
[z,X] is set
{z,X} is non empty set
{z} is non empty set
{{z,X},{z}} is non empty set
minreal . [z,X] is set
maxreal . ((minreal . (z,X)),X) is set
[(minreal . (z,X)),X] is set
{(minreal . (z,X)),X} is non empty set
{(minreal . (z,X))} is non empty set
{{(minreal . (z,X)),X},{(minreal . (z,X))}} is non empty set
maxreal . [(minreal . (z,X)),X] is set
ma is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of mi
z is Element of the carrier of mi
X is Element of the carrier of mi
L9 "/\" L9 is Element of the carrier of L
ma "/\" (L9 "/\" L9) is Element of the carrier of L
minreal . (ma,(L9 "/\" L9)) is set
[ma,(L9 "/\" L9)] is set
{ma,(L9 "/\" L9)} is non empty set
{ma} is non empty set
{{ma,(L9 "/\" L9)},{ma}} is non empty set
minreal . [ma,(L9 "/\" L9)] is set
minreal . (L9,L9) is set
[L9,L9] is set
{L9,L9} is non empty set
{L9} is non empty set
{{L9,L9},{L9}} is non empty set
minreal . [L9,L9] is set
minreal . (ma,(minreal . (L9,L9))) is set
[ma,(minreal . (L9,L9))] is set
{ma,(minreal . (L9,L9))} is non empty set
{{ma,(minreal . (L9,L9))},{ma}} is non empty set
minreal . [ma,(minreal . (L9,L9))] is set
X is Element of the carrier of Real_Lattice
X is Element of the carrier of Real_Lattice
minreal . (X,X) is set
[X,X] is set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
minreal . [X,X] is set
q is Element of the carrier of Real_Lattice
minreal . ((minreal . (X,X)),q) is set
[(minreal . (X,X)),q] is set
{(minreal . (X,X)),q} is non empty set
{(minreal . (X,X))} is non empty set
{{(minreal . (X,X)),q},{(minreal . (X,X))}} is non empty set
minreal . [(minreal . (X,X)),q] is set
ma "/\" L9 is Element of the carrier of L
minreal . ((ma "/\" L9),L9) is set
[(ma "/\" L9),L9] is set
{(ma "/\" L9),L9} is non empty set
{(ma "/\" L9)} is non empty set
{{(ma "/\" L9),L9},{(ma "/\" L9)}} is non empty set
minreal . [(ma "/\" L9),L9] is set
(ma "/\" L9) "/\" L9 is Element of the carrier of L
ma is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of L
L9 is Element of the carrier of mi
z is Element of the carrier of mi
X is Element of the carrier of mi
L9 "\/" L9 is Element of the carrier of L
ma "\/" (L9 "\/" L9) is Element of the carrier of L
maxreal . (ma,(L9 "\/" L9)) is set
[ma,(L9 "\/" L9)] is set
{ma,(L9 "\/" L9)} is non empty set
{ma} is non empty set
{{ma,(L9 "\/" L9)},{ma}} is non empty set
maxreal . [ma,(L9 "\/" L9)] is set
maxreal . (L9,L9) is set
[L9,L9] is set
{L9,L9} is non empty set
{L9} is non empty set
{{L9,L9},{L9}} is non empty set
maxreal . [L9,L9] is set
maxreal . (ma,(maxreal . (L9,L9))) is set
[ma,(maxreal . (L9,L9))] is set
{ma,(maxreal . (L9,L9))} is non empty set
{{ma,(maxreal . (L9,L9))},{ma}} is non empty set
maxreal . [ma,(maxreal . (L9,L9))] is set
X is Element of the carrier of Real_Lattice
X is Element of the carrier of Real_Lattice
maxreal . (X,X) is set
[X,X] is set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
maxreal . [X,X] is set
q is Element of the carrier of Real_Lattice
maxreal . ((maxreal . (X,X)),q) is set
[(maxreal . (X,X)),q] is set
{(maxreal . (X,X)),q} is non empty set
{(maxreal . (X,X))} is non empty set
{{(maxreal . (X,X)),q},{(maxreal . (X,X))}} is non empty set
maxreal . [(maxreal . (X,X)),q] is set
ma "\/" L9 is Element of the carrier of L
maxreal . ((ma "\/" L9),L9) is set
[(ma "\/" L9),L9] is set
{(ma "\/" L9),L9} is non empty set
{(ma "\/" L9)} is non empty set
{{(ma "\/" L9),L9},{(ma "\/" L9)}} is non empty set
maxreal . [(ma "\/" L9),L9] is set
(ma "\/" L9) "\/" L9 is Element of the carrier of L
ma is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
L9 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of (0,1)
the carrier of L9 is non empty set
bool the carrier of L9 is non empty set
L9 is Element of bool the carrier of L9
"\/" (L9,mi) is Element of the carrier of mi
z is V31() V32() ext-real Element of REAL
X is set
X is Element of the carrier of L9
X is Element of the carrier of mi
q is V31() V32() ext-real Element of REAL
min (q,z) is V31() V32() ext-real set
minreal . (X,("\/" (L9,mi))) is set
[X,("\/" (L9,mi))] is set
{X,("\/" (L9,mi))} is non empty set
{X} is non empty set
{{X,("\/" (L9,mi))},{X}} is non empty set
minreal . [X,("\/" (L9,mi))] is set
[X,("\/" (L9,mi))] is Element of [: the carrier of mi, the carrier of mi:]
[: the carrier of mi, the carrier of mi:] is non empty set
(minreal || A) . [X,("\/" (L9,mi))] is set
(minreal || A) . (X,("\/" (L9,mi))) is set
(minreal || A) . [X,("\/" (L9,mi))] is set
X "/\" ("\/" (L9,mi)) is Element of the carrier of mi
z + q is V31() V32() ext-real Element of REAL
(1 / 2) + z is V31() V32() ext-real Element of REAL
q9 is V31() V32() ext-real Element of REAL
X is Element of the carrier of mi
X is V31() V32() ext-real Element of REAL
L9 is Element of the carrier of mi
L9 "/\" X is Element of the carrier of mi
(minreal || A) . (L9,X) is set
[L9,X] is set
{L9,X} is non empty set
{L9} is non empty set
{{L9,X},{L9}} is non empty set
(minreal || A) . [L9,X] is set
[L9,X] is Element of [: the carrier of mi, the carrier of mi:]
minreal . [L9,X] is set
minreal . (L9,X) is set
minreal . [L9,X] is set
min (0,X) is V31() V32() ext-real set
X is Element of the carrier of mi
L9 is Element of the carrier of mi
z is V31() V32() ext-real Element of REAL
z is set
z is Element of bool the carrier of L9
X is Element of the carrier of mi
X is V31() V32() ext-real Element of REAL
X is Element of bool the carrier of L9
"/\" (X,mi) is Element of the carrier of mi
{ b1 where b1 is Element of the carrier of mi : b1 is_less_than X } is set
"\/" ( { b1 where b1 is Element of the carrier of mi : b1 is_less_than X } ,mi) is Element of the carrier of mi
X + X is V31() V32() ext-real Element of REAL
(1 / 2) + X is V31() V32() ext-real Element of REAL
(X + X) / 2 is V31() V32() ext-real Element of REAL
((1 / 2) + X) / 2 is V31() V32() ext-real Element of REAL
(((1 / 2) + X) / 2) + X is V31() V32() ext-real Element of REAL
X + 1 is V31() V32() ext-real Element of REAL
X + (1 / 2) is V31() V32() ext-real Element of REAL
(1 / 2) + (1 / 2) is V31() V32() ext-real non negative Element of REAL
q is Element of the carrier of mi
X "/\" q is Element of the carrier of mi
(minreal || A) . (X,q) is set
[X,q] is set
{X,q} is non empty set
{X} is non empty set
{{X,q},{X}} is non empty set
(minreal || A) . [X,q] is set
[X,q] is Element of [: the carrier of mi, the carrier of mi:]
[: the carrier of mi, the carrier of mi:] is non empty set
minreal . [X,q] is set
minreal . (X,q) is set
minreal . [X,q] is set
min (X,(((1 / 2) + X) / 2)) is V31() V32() ext-real set
L9 is Element of the carrier of mi
X "/\" L9 is Element of the carrier of mi
(minreal || A) . (X,L9) is set
[X,L9] is set
{X,L9} is non empty set
{X} is non empty set
{{X,L9},{X}} is non empty set
(minreal || A) . [X,L9] is set
[X,L9] is Element of [: the carrier of mi, the carrier of mi:]
[: the carrier of mi, the carrier of mi:] is non empty set
minreal . [X,L9] is set
minreal . (X,L9) is set
minreal . [X,L9] is set
min (X,(1 / 2)) is V31() V32() ext-real set
X is Element of the carrier of mi
X is V31() V32() ext-real Element of REAL
L9 "/\" X is Element of the carrier of mi
(minreal || A) . (L9,X) is set
[L9,X] is set
{L9,X} is non empty set
{L9} is non empty set
{{L9,X},{L9}} is non empty set
(minreal || A) . [L9,X] is set
[L9,X] is Element of [: the carrier of mi, the carrier of mi:]
minreal . [L9,X] is set
minreal . (L9,X) is set
minreal . [L9,X] is set
min ((1 / 2),X) is V31() V32() ext-real set
q is V31() V32() ext-real Element of REAL
"/\" (X,mi) is Element of the carrier of mi
{ b1 where b1 is Element of the carrier of mi : b1 is_less_than X } is set
"\/" ( { b1 where b1 is Element of the carrier of mi : b1 is_less_than X } ,mi) is Element of the carrier of mi
L9 is Element of bool the carrier of L9
"/\" (L9,mi) is Element of the carrier of mi
{ b1 where b1 is Element of the carrier of mi : b1 is_less_than L9 } is set
"\/" ( { b1 where b1 is Element of the carrier of mi : b1 is_less_than L9 } ,mi) is Element of the carrier of mi
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of (0,1)
{0,1} is non empty V36() V37() V38() V39() V40() V41() Element of bool REAL
2 is non empty natural V31() V32() ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT
1 / 2 is V31() V32() ext-real non negative Element of REAL
].0,(1 / 2).[ is V36() V37() V38() Element of bool REAL
{0,1} \/ ].0,(1 / 2).[ is non empty V36() V37() V38() Element of bool REAL
{1} is non empty V36() V37() V38() V39() V40() V41() Element of bool REAL
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( 0 <= b1 & not 1 / 2 <= b1 ) } is set
{1} \/ { b1 where b1 is V31() V32() ext-real Element of REAL : ( 0 <= b1 & not 1 / 2 <= b1 ) } is non empty set
A is set
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( not b1 <= 0 & not 1 / 2 <= b1 ) } is set
B is V31() V32() ext-real Element of REAL
A is set
B is V31() V32() ext-real Element of REAL
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( not b1 <= 0 & not 1 / 2 <= b1 ) } is set
{ b1 where b1 is V31() V32() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
[.0,1.] is V36() V37() V38() Element of bool REAL
A is non empty set
B is Element of A
Ma is V31() V32() ext-real Element of REAL
the L_meet of (0,1) is V1() V4([: the carrier of (0,1), the carrier of (0,1):]) V5( the carrier of (0,1)) Function-like V18([: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1)) Element of bool [:[: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1):]
the carrier of (0,1) is non empty set
[: the carrier of (0,1), the carrier of (0,1):] is non empty set
[:[: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1):] is non empty set
bool [:[: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1):] is non empty set
minreal || [.0,1.] is V1() Function-like set
[:[.0,1.],[.0,1.]:] is set
K5(minreal,[:[.0,1.],[.0,1.]:]) is V1() set
maxreal || A is V1() Function-like set
[:A,A:] is non empty set
K5(maxreal,[:A,A:]) is V1() set
minreal || A is V1() Function-like set
K5(minreal,[:A,A:]) is V1() set
the L_join of (0,1) is V1() V4([: the carrier of (0,1), the carrier of (0,1):]) V5( the carrier of (0,1)) Function-like V18([: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1)) Element of bool [:[: the carrier of (0,1), the carrier of (0,1):], the carrier of (0,1):]
maxreal || [.0,1.] is V1() Function-like set
K5(maxreal,[:[.0,1.],[.0,1.]:]) is V1() set
[:[:A,A:],A:] is non empty set
bool [:[:A,A:],A:] is non empty set
ma is set
B is non empty set
mi is V31() V32() ext-real Element of REAL
mi + (1 / 2) is V31() V32() ext-real Element of REAL
(1 / 2) + 1 is non empty V31() V32() ext-real positive non negative Element of REAL
[:B,B:] is non empty set
[:[:B,B:],A:] is non empty set
bool [:[:B,B:],A:] is non empty set
Ma is V1() V4([:A,A:]) V5(A) Function-like V18([:A,A:],A) Element of bool [:[:A,A:],A:]
Ma || B is V1() Function-like set
K5(Ma,[:B,B:]) is V1() set
Mi is V1() V4([:A,A:]) V5(A) Function-like V18([:A,A:],A) Element of bool [:[:A,A:],A:]
Mi || B is V1() Function-like set
K5(Mi,[:B,B:]) is V1() set
ma is V1() V4([:B,B:]) V5(A) Function-like V18([:B,B:],A) Element of bool [:[:B,B:],A:]
dom ma is V1() V4(B) V5(B) Element of bool [:B,B:]
bool [:B,B:] is non empty set
L is set
mi is set
ma is set
[mi,ma] is set
{mi,ma} is non empty set
{mi} is non empty set
{{mi,ma},{mi}} is non empty set
ma . L is set
Ma . [mi,ma] is set
maxreal . (mi,ma) is set
maxreal . [mi,ma] is set
max (1,1) is V31() V32() ext-real set
L9 is V31() V32() ext-real Element of REAL
ma . L is set
Ma . [mi,ma] is set
maxreal . (mi,ma) is set
maxreal . [mi,ma] is set
max (1,L9) is V31() V32() ext-real set
ma . L is set
ma . L is set
L9 is V31() V32() ext-real Element of REAL
ma . L is set
Ma . [mi,ma] is set
maxreal . (mi,ma) is set
maxreal . [mi,ma] is set
max (L9,1) is V31() V32() ext-real set
L9 is V31() V32() ext-real Element of REAL
ma . L is set
Ma . [mi,ma] is set
maxreal . (mi,ma) is set
maxreal . [mi,ma] is set
max (L9,L9) is V31() V32() ext-real set
ma . L is set
ma . L is set
ma . L is set
ma . L is set
mi is V1() V4([:B,B:]) V5(A) Function-like V18([:B,B:],A) Element of bool [:[:B,B:],A:]
dom mi is V1() V4(B) V5(B) Element of bool [:B,B:]
L is set
mi is set
ma is set
[mi,ma] is set
{mi,ma} is non empty set
{mi} is non empty set
{{mi,ma},{mi}} is non empty set
mi . L is set
Mi . [mi,ma] is set
minreal . (mi,ma) is set
minreal . [mi,ma] is set
min (1,1) is V31() V32() ext-real set
L9 is V31() V32() ext-real Element of REAL
mi . L is set
Mi . [mi,ma] is set
minreal . (mi,ma) is set
minreal . [mi,ma] is set
min (1,L9) is V31() V32() ext-real set
mi . L is set
mi . L is set
L9 is V31() V32() ext-real Element of REAL
mi . L is set
Mi . [mi,ma] is set
minreal . (mi,ma) is set
minreal . [mi,ma] is set
min (L9,1) is V31() V32() ext-real set
L9 is V31() V32() ext-real Element of REAL
mi . L is set
Mi . [mi,ma] is set
minreal . (mi,ma) is set
minreal . [mi,ma] is set
min (L9,L9) is V31() V32() ext-real set
mi . L is set
mi . L is set
mi . L is set
mi . L is set
[:[:B,B:],B:] is non empty set
bool [:[:B,B:],B:] is non empty set
ma is V1() V4([:B,B:]) V5(B) Function-like V18([:B,B:],B) Element of bool [:[:B,B:],B:]
mi is V1() V4([:B,B:]) V5(B) Function-like V18([:B,B:],B) Element of bool [:[:B,B:],B:]
LattStr(# B,ma,mi #) is non empty strict LattStr
L9 is non empty LattStr
the carrier of L9 is non empty set
L9 is Element of the carrier of L9
L9 is Element of the carrier of L9
[L9,L9] is Element of [: the carrier of L9, the carrier of L9:]
[: the carrier of L9, the carrier of L9:] is non empty set
{L9,L9} is non empty set
{L9} is non empty set
{{L9,L9},{L9}} is non empty set
L9 "\/" L9 is Element of the carrier of L9
the L_join of L9 is V1() V4([: the carrier of L9, the carrier of L9:]) V5( the carrier of L9) Function-like V18([: the carrier of L9, the carrier of L9:], the carrier of L9) Element of bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:]
[:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is non empty set
bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:] is non empty set
the L_join of L9 . (L9,L9) is Element of the carrier of L9
[L9,L9] is set
the L_join of L9 . [L9,L9] is set
(maxreal || A) . [L9,L9] is set
maxreal . (L9,L9) is set
maxreal . [L9,L9] is set
L9 "/\" L9 is Element of the carrier of L9
the L_meet of L9 is V1() V4([: the carrier of L9, the carrier of L9:]) V5( the carrier of L9) Function-like V18([: the carrier of L9, the carrier of L9:], the carrier of L9) Element of bool [:[: the carrier of L9, the carrier of L9:], the carrier of L9:]
the L_meet of L9 . (L9,L9) is Element of the carrier of L9
the L_meet of L9 . [L9,L9] is set
(minreal || A) . [L9,L9] is set
minreal . (L9,L9) is set
minreal . [L9,L9] is set
L9 is Element of B
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of L is non empty set
L9 is Element of B
L9 is V31() V32() ext-real Element of REAL
L9 + (1 / 2) is V31() V32() ext-real Element of REAL
(1 / 2) + 1 is non empty V31() V32() ext-real positive non negative Element of REAL
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of L is non empty set
L9 is Element of B
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of L is non empty set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of L is non empty set
L9 is Element of the carrier of L9
L9 is Element of the carrier of L9
z is Element of the carrier of L
X is Element of the carrier of L
L9 "\/" L9 is Element of the carrier of L9
maxreal . (L9,L9) is set
[L9,L9] is set
{L9,L9} is non empty set
{L9} is non empty set
{{L9,L9},{L9}} is non empty set
maxreal . [L9,L9] is set
X is Element of the carrier of Real_Lattice
X is Element of the carrier of Real_Lattice
maxreal . (X,X) is set
[X,X] is set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
maxreal . [X,X] is set
L9 "\/" L9 is Element of the carrier of L9
L9 is Element of the carrier of L9
L9 is Element of the carrier of L9
z is Element of the carrier of L
X is Element of the carrier of L
L9 "\/" L9 is Element of the carrier of L9
L9 "/\" (L9 "\/" L9) is Element of the carrier of L9
minreal . (L9,(L9 "\/" L9)) is set
[L9,(L9 "\/" L9)] is set
{L9,(L9 "\/" L9)} is non empty set
{L9} is non empty set
{{L9,(L9 "\/" L9)},{L9}} is non empty set
minreal . [L9,(L9 "\/" L9)] is set
X is Element of the carrier of Real_Lattice
X is Element of the carrier of Real_Lattice
maxreal . (X,X) is set
[X,X] is set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
maxreal . [X,X] is set
minreal . (X,(maxreal . (X,X))) is set
[X,(maxreal . (X,X))] is set
{X,(maxreal . (X,X))} is non empty set
{{X,(maxreal . (X,X))},{X}} is non empty set
minreal . [X,(maxreal . (X,X))] is set
L9 is Element of the carrier of L9
L9 is Element of the carrier of L9
z is Element of the carrier of L
X is Element of the carrier of L
L9 "/\" L9 is Element of the carrier of L9
minreal . (L9,L9) is set
[L9,L9] is set
{L9,L9} is non empty set
{L9} is non empty set
{{L9,L9},{L9}} is non empty set
minreal . [L9,L9] is set
X is Element of the carrier of Real_Lattice
X is Element of the carrier of Real_Lattice
minreal . (X,X) is set
[X,X] is set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
minreal . [X,X] is set
L9 "/\" L9 is Element of the carrier of L9
L9 is Element of the carrier of L9
L9 is Element of the carrier of L9
z is Element of the carrier of L
X is Element of the carrier of L
L9 "/\" L9 is Element of the carrier of L9
(L9 "/\" L9) "\/" L9 is Element of the carrier of L9
maxreal . ((L9 "/\" L9),L9) is set
[(L9 "/\" L9),L9] is set
{(L9 "/\" L9),L9} is non empty set
{(L9 "/\" L9)} is non empty set
{{(L9 "/\" L9),L9},{(L9 "/\" L9)}} is non empty set
maxreal . [(L9 "/\" L9),L9] is set
X is Element of the carrier of Real_Lattice
X is Element of the carrier of Real_Lattice
minreal . (X,X) is set
[X,X] is set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
minreal . [X,X] is set
maxreal . ((minreal . (X,X)),X) is set
[(minreal . (X,X)),X] is set
{(minreal . (X,X)),X} is non empty set
{(minreal . (X,X))} is non empty set
{{(minreal . (X,X)),X},{(minreal . (X,X))}} is non empty set
maxreal . [(minreal . (X,X)),X] is set
L9 is Element of the carrier of L9
L9 is Element of the carrier of L9
z is Element of the carrier of L9
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L9 "/\" z is Element of the carrier of L9
L9 "/\" (L9 "/\" z) is Element of the carrier of L9
minreal . (L9,(L9 "/\" z)) is set
[L9,(L9 "/\" z)] is set
{L9,(L9 "/\" z)} is non empty set
{L9} is non empty set
{{L9,(L9 "/\" z)},{L9}} is non empty set
minreal . [L9,(L9 "/\" z)] is set
minreal . (L9,z) is set
[L9,z] is set
{L9,z} is non empty set
{L9} is non empty set
{{L9,z},{L9}} is non empty set
minreal . [L9,z] is set
minreal . (L9,(minreal . (L9,z))) is set
[L9,(minreal . (L9,z))] is set
{L9,(minreal . (L9,z))} is non empty set
{{L9,(minreal . (L9,z))},{L9}} is non empty set
minreal . [L9,(minreal . (L9,z))] is set
q is Element of the carrier of Real_Lattice
q9 is Element of the carrier of Real_Lattice
minreal . (q,q9) is set
[q,q9] is set
{q,q9} is non empty set
{q} is non empty set
{{q,q9},{q}} is non empty set
minreal . [q,q9] is set
c is Element of the carrier of Real_Lattice
minreal . ((minreal . (q,q9)),c) is set
[(minreal . (q,q9)),c] is set
{(minreal . (q,q9)),c} is non empty set
{(minreal . (q,q9))} is non empty set
{{(minreal . (q,q9)),c},{(minreal . (q,q9))}} is non empty set
minreal . [(minreal . (q,q9)),c] is set
L9 "/\" L9 is Element of the carrier of L9
minreal . ((L9 "/\" L9),z) is set
[(L9 "/\" L9),z] is set
{(L9 "/\" L9),z} is non empty set
{(L9 "/\" L9)} is non empty set
{{(L9 "/\" L9),z},{(L9 "/\" L9)}} is non empty set
minreal . [(L9 "/\" L9),z] is set
(L9 "/\" L9) "/\" z is Element of the carrier of L9
L9 is Element of the carrier of L9
L9 is Element of the carrier of L9
z is Element of the carrier of L9
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L9 "\/" z is Element of the carrier of L9
L9 "\/" (L9 "\/" z) is Element of the carrier of L9
maxreal . (L9,(L9 "\/" z)) is set
[L9,(L9 "\/" z)] is set
{L9,(L9 "\/" z)} is non empty set
{L9} is non empty set
{{L9,(L9 "\/" z)},{L9}} is non empty set
maxreal . [L9,(L9 "\/" z)] is set
maxreal . (L9,z) is set
[L9,z] is set
{L9,z} is non empty set
{L9} is non empty set
{{L9,z},{L9}} is non empty set
maxreal . [L9,z] is set
maxreal . (L9,(maxreal . (L9,z))) is set
[L9,(maxreal . (L9,z))] is set
{L9,(maxreal . (L9,z))} is non empty set
{{L9,(maxreal . (L9,z))},{L9}} is non empty set
maxreal . [L9,(maxreal . (L9,z))] is set
q is Element of the carrier of Real_Lattice
q9 is Element of the carrier of Real_Lattice
maxreal . (q,q9) is set
[q,q9] is set
{q,q9} is non empty set
{q} is non empty set
{{q,q9},{q}} is non empty set
maxreal . [q,q9] is set
c is Element of the carrier of Real_Lattice
maxreal . ((maxreal . (q,q9)),c) is set
[(maxreal . (q,q9)),c] is set
{(maxreal . (q,q9)),c} is non empty set
{(maxreal . (q,q9))} is non empty set
{{(maxreal . (q,q9)),c},{(maxreal . (q,q9))}} is non empty set
maxreal . [(maxreal . (q,q9)),c] is set
L9 "\/" L9 is Element of the carrier of L9
maxreal . ((L9 "\/" L9),z) is set
[(L9 "\/" L9),z] is set
{(L9 "\/" L9),z} is non empty set
{(L9 "\/" L9)} is non empty set
{{(L9 "\/" L9),z},{(L9 "\/" L9)}} is non empty set
maxreal . [(L9 "\/" L9),z] is set
(L9 "\/" L9) "\/" z is Element of the carrier of L9
L9 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
L9 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of (0,1)
the carrier of L9 is non empty set
bool the carrier of L9 is non empty set
z is Element of bool the carrier of L9
"/\" (z,L) is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_less_than z } is set
"\/" ( { b1 where b1 is Element of the carrier of L : b1 is_less_than z } ,L) is Element of the carrier of L
X is V31() V32() ext-real Element of REAL
X is set
q is Element of the carrier of L9
q9 is Element of the carrier of L
c is V31() V32() ext-real Element of REAL
min (c,X) is V31() V32() ext-real set
minreal . (q9,("/\" (z,L))) is set
[q9,("/\" (z,L))] is set
{q9,("/\" (z,L))} is non empty set
{q9} is non empty set
{{q9,("/\" (z,L))},{q9}} is non empty set
minreal . [q9,("/\" (z,L))] is set
[q9,("/\" (z,L))] is Element of [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
(minreal || A) . [q9,("/\" (z,L))] is set
(minreal || A) . (q9,("/\" (z,L))) is set
(minreal || A) . [q9,("/\" (z,L))] is set
q9 "/\" ("/\" (z,L)) is Element of the carrier of L
X + (1 / 2) is V31() V32() ext-real Element of REAL
c + X is V31() V32() ext-real Element of REAL
c25 is V31() V32() ext-real Element of REAL
X is Element of the carrier of L
q is V31() V32() ext-real Element of REAL
X is Element of the carrier of L
X "/\" X is Element of the carrier of L
(minreal || A) . (X,X) is set
[X,X] is set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
(minreal || A) . [X,X] is set
[X,X] is Element of [: the carrier of L, the carrier of L:]
minreal . [X,X] is set
minreal . (X,X) is set
minreal . [X,X] is set
min (q,1) is V31() V32() ext-real set
X is Element of the carrier of L
X is Element of the carrier of L
X is V31() V32() ext-real Element of REAL
X is set
X is Element of bool the carrier of L9
q is Element of the carrier of L
q9 is V31() V32() ext-real Element of REAL
X is Element of bool the carrier of L9
(1 / 2) + q9 is V31() V32() ext-real Element of REAL
1 + 1 is non empty V31() V32() ext-real positive non negative Element of REAL
((1 / 2) + q9) / 2 is V31() V32() ext-real Element of REAL
(1 + 1) / 2 is V31() V32() ext-real non negative Element of REAL
q9 + q9 is V31() V32() ext-real Element of REAL
(q9 + q9) / 2 is V31() V32() ext-real Element of REAL
(1 / 2) + (1 / 2) is V31() V32() ext-real non negative Element of REAL
q9 + (1 / 2) is V31() V32() ext-real Element of REAL
"\/" (X,L) is Element of the carrier of L
c is Element of the carrier of L
c "/\" q is Element of the carrier of L
(minreal || A) . (c,q) is set
[c,q] is set
{c,q} is non empty set
{c} is non empty set
{{c,q},{c}} is non empty set
(minreal || A) . [c,q] is set
[c,q] is Element of [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
minreal . [c,q] is set
minreal . (c,q) is set
minreal . [c,q] is set
min ((((1 / 2) + q9) / 2),q9) is V31() V32() ext-real set
z is Element of the carrier of L
z "/\" q is Element of the carrier of L
(minreal || A) . (z,q) is set
[z,q] is set
{z,q} is non empty set
{z} is non empty set
{{z,q},{z}} is non empty set
(minreal || A) . [z,q] is set
[z,q] is Element of [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
minreal . [z,q] is set
minreal . (z,q) is set
minreal . [z,q] is set
min ((1 / 2),q9) is V31() V32() ext-real set
q is Element of the carrier of L
q9 is V31() V32() ext-real Element of REAL
q "/\" z is Element of the carrier of L
(minreal || A) . (q,z) is set
[q,z] is set
{q,z} is non empty set
{q} is non empty set
{{q,z},{q}} is non empty set
(minreal || A) . [q,z] is set
[q,z] is Element of [: the carrier of L, the carrier of L:]
minreal . [q,z] is set
minreal . (q,z) is set
minreal . [q,z] is set
min (q9,(1 / 2)) is V31() V32() ext-real set
c is V31() V32() ext-real Element of REAL
"\/" (X,L) is Element of the carrier of L
z is Element of bool the carrier of L9
"\/" (z,L) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
c2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of (0,1)