:: MSUALG_7 semantic presentation

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

c

id c

A is set

(id c

c

[:(c

bool [:(c

id (c

A is V1() V4(L) Function-like V14(L) ManySortedRelation of c

B is set

c

[:(c

bool [:(c

A . B is set

Ma is V1() V4(c

id (c

L is non empty set

c

[|c

A is set

[|c

c

[:(c

bool [:(c

A is V1() V4(L) Function-like V14(L) ManySortedRelation of c

B is set

c

[:(c

bool [:(c

A . B is set

Ma is V1() V4(c

nabla (c

L is non empty set

c

EqRelLatt c

the carrier of (EqRelLatt c

[|c

R is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

A is Element of the carrier of (EqRelLatt c

B is Element of the carrier of (EqRelLatt c

A "\/" B is Element of the carrier of (EqRelLatt c

B "\/" A is Element of the carrier of (EqRelLatt c

Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

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 c

Mi is set

c

[:(c

bool [:(c

Ma is Element of L

R . Ma is V1() V4(c

c

[:(c

bool [:(c

Ma . Ma is V1() V4(c

(R \/ Ma) . Mi is set

R . Mi is set

Ma . Mi is set

(R . Mi) \/ (Ma . Mi) is set

[:(c

nabla (c

ma is V1() V4(c

(nabla (c

(R "\/" Ma) . Mi is set

Mi is V1() V4(c

EqCl Mi is V1() V4(c

mi is V1() V4(L) Function-like V14(L) ManySortedRelation of c

EqCl mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

the L_join of (EqRelLatt c

[: the carrier of (EqRelLatt c

[:[: the carrier of (EqRelLatt c

bool [:[: the carrier of (EqRelLatt c

the L_join of (EqRelLatt c

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

R is Element of the carrier of (EqRelLatt c

id c

R is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

A is Element of the carrier of (EqRelLatt c

B is Element of the carrier of (EqRelLatt c

A "/\" B is Element of the carrier of (EqRelLatt c

B "/\" A is Element of the carrier of (EqRelLatt c

Mi is set

c

[:(c

bool [:(c

Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Ma is Element of L

Ma . Ma is V1() V4(c

c

[:(c

bool [:(c

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 (c

Mi is V1() V4(c

(id (c

the L_meet of (EqRelLatt c

[: the carrier of (EqRelLatt c

[:[: the carrier of (EqRelLatt c

bool [:[: the carrier of (EqRelLatt c

the L_meet of (EqRelLatt c

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

R is Element of the carrier of (EqRelLatt c

L is non empty set

c

EqRelLatt c

Bottom (EqRelLatt c

the carrier of (EqRelLatt c

id c

A is Element of the carrier of (EqRelLatt c

B is Element of the carrier of (EqRelLatt c

Ma is set

c

[:(c

bool [:(c

Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Mi is Element of L

Mi . Mi is V1() V4(c

c

[:(c

bool [:(c

Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

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 (c

ma is V1() V4(c

(id (c

A "/\" B is Element of the carrier of (EqRelLatt c

the L_meet of (EqRelLatt c

[: the carrier of (EqRelLatt c

[:[: the carrier of (EqRelLatt c

bool [:[: the carrier of (EqRelLatt c

the L_meet of (EqRelLatt c

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

B "/\" A is Element of the carrier of (EqRelLatt c

L is non empty set

c

EqRelLatt c

Top (EqRelLatt c

the carrier of (EqRelLatt c

[|c

A is Element of the carrier of (EqRelLatt c

B is Element of the carrier of (EqRelLatt c

Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

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 c

Ma is set

c

[:(c

bool [:(c

Mi is Element of L

Ma . Mi is V1() V4(c

c

[:(c

bool [:(c

Mi . Mi is V1() V4(c

(Ma \/ Mi) . Ma is set

Ma . Ma is set

Mi . Ma is set

(Ma . Ma) \/ (Mi . Ma) is set

[:(c

nabla (c

mi is V1() V4(c

(nabla (c

(Ma "\/" Mi) . Ma is set

ma is V1() V4(c

EqCl ma is V1() V4(c

L is V1() V4(L) Function-like V14(L) ManySortedRelation of c

EqCl L is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

A "\/" B is Element of the carrier of (EqRelLatt c

the L_join of (EqRelLatt c

[: the carrier of (EqRelLatt c

[:[: the carrier of (EqRelLatt c

bool [:[: the carrier of (EqRelLatt c

the L_join of (EqRelLatt c

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

B "\/" A is Element of the carrier of (EqRelLatt c

L is non empty set

c

EqRelLatt c

the carrier of (EqRelLatt c

bool the carrier of (EqRelLatt c

[|c

Bool [|c

bool (Bool [|c

R is Element of bool the carrier of (EqRelLatt c

A is set

Ma is set

Mi is Element of L

c

B is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

B . Mi is V1() V4(c

[:(c

bool [:(c

B . Ma is set

[|c

Bool [|c

bool the carrier of (EqRelLatt c

bool (bool the carrier of (EqRelLatt c

bool (Bool [|c

bool (Bool [|c

bool (bool (Bool [|c

L is non empty set

c

EqRelLatt c

the carrier of (EqRelLatt c

R is Element of the carrier of (EqRelLatt c

A is Element of the carrier of (EqRelLatt c

B is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

B /\ Ma is V1() V4(L) Function-like V14(L) set

the L_meet of (EqRelLatt c

[: the carrier of (EqRelLatt c

[:[: the carrier of (EqRelLatt c

bool [:[: the carrier of (EqRelLatt c

the L_meet of (EqRelLatt c

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

R "/\" A is Element of the carrier of (EqRelLatt c

R "/\" A is Element of the carrier of (EqRelLatt c

the L_meet of (EqRelLatt c

[: the carrier of (EqRelLatt c

[:[: the carrier of (EqRelLatt c

bool [:[: the carrier of (EqRelLatt c

the L_meet of (EqRelLatt c

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

B /\ Ma is V1() V4(L) Function-like V14(L) set

L is non empty set

c

EqRelLatt c

the carrier of (EqRelLatt c

bool the carrier of (EqRelLatt c

[|c

Bool [|c

bool (Bool [|c

R is Element of bool the carrier of (EqRelLatt c

A is Element of bool (Bool [|c

|:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c

K200(L,[|c

meet |:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of [|c

B is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Bool [|c

Ma is set

|:A:| . Ma is set

{ (b

Mi is V1() V4(L) Function-like V14(L) Element of Bool [|c

Mi . Ma is set

meet (|:A:| . Ma) is set

Ma . Ma is set

Mi is set

[|c

bool ([|c

bool (bool ([|c

(meet |:A:|) . Ma is set

B . Ma is set

Mi is Element of bool (bool ([|c

Intersect Mi is Element of bool ([|c

L is non empty set

c

EqRelLatt c

the carrier of (EqRelLatt c

bool the carrier of (EqRelLatt c

[|c

Bool [|c

bool (Bool [|c

R is Element of bool the carrier of (EqRelLatt c

A is Element of bool (Bool [|c

|:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c

K200(L,[|c

meet |:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of [|c

Ma is set

(meet |:A:|) . Ma is set

[|c

c

[:(c

bool [:(c

Ma is set

c

[:(c

bool [:(c

Ma is V1() V4(L) Function-like V14(L) ManySortedRelation of c

Ma . Ma is set

Mi is V1() V4(c

bool (bool [:(c

ma is Element of L

|:A:| . ma is Element of bool (bool ([|c

[|c

bool ([|c

bool (bool ([|c

[|c

bool ([|c

bool (bool ([|c

|:A:| . Ma is set

L is Element of bool (bool ([|c

Intersect L is Element of bool ([|c

Mi is non empty Element of bool (Bool [|c

|:Mi:| is V1() non-empty V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c

mi is Element of bool (bool [:(c

|:Mi:| . Ma is set

Bool [|c

{ (b

ma is set

mi is Element of bool (bool [:(c

L9 is V1() V4(L) Function-like V14(L) Element of Bool [|c

L9 . Ma is set

L9 is V1() V4(c

meet mi is V1() V4(c

L is non empty LattStr

the carrier of L is non empty set

bool the carrier of L is non empty set

c

c

{ b

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

c

EqRelLatt c

the carrier of (EqRelLatt c

bool the carrier of (EqRelLatt c

R is Element of bool the carrier of (EqRelLatt c

[|c

Bool [|c

bool (Bool [|c

Top (EqRelLatt c

B is Element of the carrier of (EqRelLatt c

Ma is Element of the carrier of (EqRelLatt c

Ma is Element of the carrier of (EqRelLatt c

A is Element of bool (Bool [|c

|:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c

K200(L,[|c

meet |:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of [|c

B is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Mi is Element of the carrier of (EqRelLatt c

Ma is Element of the carrier of (EqRelLatt c

Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Ma is Element of the carrier of (EqRelLatt c

mi is set

[|c

bool ([|c

bool (bool ([|c

|:A:| . mi is set

(meet |:A:|) . mi is set

ma is non empty Element of bool (Bool [|c

|:ma:| is V1() non-empty V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c

L is set

|:ma:| . mi is set

Bool [|c

{ (b

mi is V1() V4(L) Function-like V14(L) Element of Bool [|c

mi . mi is set

ma is Element of the carrier of (EqRelLatt c

Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

L9 is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Mi . mi is set

meet (|:A:| . mi) is set

L is Element of bool (bool ([|c

Intersect L is Element of bool ([|c

Ma is Element of the carrier of (EqRelLatt c

L is non empty set

c

EqRelLatt c

L is non empty set

c

EqRelLatt c

the carrier of (EqRelLatt c

bool the carrier of (EqRelLatt c

[|c

Bool [|c

bool (Bool [|c

R is Element of bool the carrier of (EqRelLatt c

"/\" (R,(EqRelLatt c

{ b

"\/" ( { b

A is Element of bool (Bool [|c

|:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c

K200(L,[|c

meet |:A:| is V1() V4(L) Function-like V14(L) ManySortedSubset of [|c

B is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

Mi is Element of the carrier of (EqRelLatt c

Ma is non empty Element of bool (Bool [|c

|:Ma:| is V1() non-empty V4(L) Function-like V14(L) ManySortedSubset of K200(L,[|c

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,[|c

mi is set

L . mi is set

|:A:| . mi is set

|:Ma:| . mi is set

Bool [|c

{ (b

ma is V1() V4(L) Function-like V14(L) Element of Bool [|c

ma . mi is set

L9 is Element of the carrier of (EqRelLatt c

ma is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

L9 is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

ma . mi is set

Mi is Element of the carrier of (EqRelLatt c

Ma is Element of the carrier of (EqRelLatt c

Mi is V1() V4(L) Function-like V14(L) MSEquivalence_Relation-like ManySortedRelation of c

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

c

the carrier of c

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 c

Ma is Element of the carrier of c

B "\/" Ma is Element of the carrier of c

B "/\" Ma is Element of the carrier of c

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 c

[: the carrier of c

K5( the L_join of L,[: the carrier of c

[B,Ma] is Element of [: the carrier of c

{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 c

the L_join of c

[:[: the carrier of c

bool [:[: the carrier of c

the L_join of c

[B,Ma] is set

the L_join of c

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 c

K5( the L_meet of L,[: the carrier of c

( the L_meet of L || the carrier of c

the L_meet of c

the L_meet of c

the L_meet of c

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

c

the carrier of c

bool the carrier of c

R is Element of bool the carrier of c

A is Element of the carrier of L

B is Element of the carrier of c

Ma is Element of the carrier of c

Mi is Element of the carrier of L

B "/\" Ma is Element of the carrier of c

A "/\" Mi is Element of the carrier of L

Ma is Element of the carrier of L

Mi is Element of the carrier of c

A "/\" Ma is Element of the carrier of L

B "/\" Mi is Element of the carrier of c

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

c

the carrier of c

bool the carrier of c

R is Element of bool the carrier of c

A is Element of the carrier of L

B is Element of the carrier of c

Ma is Element of the carrier of c

Mi is Element of the carrier of L

Ma "/\" B is Element of the carrier of c

Mi "/\" A is Element of the carrier of L

Ma is Element of the carrier of L

Mi is Element of the carrier of c

Ma "/\" A is Element of the carrier of L

Mi "/\" B is Element of the carrier of c

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

c

the carrier of c

bool the carrier of c

R is Element of bool the carrier of c

"/\" (R,L) is Element of the carrier of L

the carrier of L is non empty set

{ b

"\/" ( { b

B is Element of the carrier of c

Ma is Element of the carrier of c

Mi is Element of the carrier of L

Ma "/\" B is Element of the carrier of c

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

c

the carrier of c

bool the carrier of c

R is Element of bool the carrier of c

"\/" (R,L) is Element of the carrier of L

the carrier of L is non empty set

B is Element of the carrier of c

Ma is Element of the carrier of c

Mi is Element of the carrier of L

B "/\" Ma is Element of the carrier of c

("\/" (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

c

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

c

c

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

c

the carrier of c

bool the carrier of c

A is Element of bool the carrier of c

"/\" (A,L) is Element of the carrier of L

the carrier of L is non empty set

{ b

"\/" ( { b

"/\" (A,c

{ b

"\/" ( { b

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

c

the carrier of c

bool the carrier of c

A is Element of bool the carrier of c

"\/" (A,L) is Element of the carrier of L

the carrier of L is non empty set

"\/" (A,c

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

c

the carrier of c

bool the carrier of c

R is Element of bool the carrier of L

A is Element of bool the carrier of c

"/\" (R,L) is Element of the carrier of L

{ b

"\/" ( { b

"/\" (A,c

{ b

"\/" ( { 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

bool the carrier of L is non empty set

c

the carrier of c

bool the carrier of c

R is Element of bool the carrier of L

A is Element of bool the carrier of c

"\/" (R,L) is Element of the carrier of L

"\/" (A,c

L is V31() V32() ext-real Element of REAL

c

[.L,c

maxreal || [.L,c

[:[.L,c

K5(maxreal,[:[.L,c

minreal || [.L,c

K5(minreal,[:[.L,c

{ b

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

c

(L,c

[.L,c

the carrier of (L,c

the L_meet of (L,c

[: the carrier of (L,c

[:[: the carrier of (L,c

bool [:[: the carrier of (L,c

minreal || [.L,c

[:[.L,c

K5(minreal,[:[.L,c

bool the carrier of (L,c

Mi is Element of bool the carrier of (L,c

{ b

Ma is Element of the carrier of (L,c

Mi is Element of the carrier of (L,c

Mi is Element of the carrier of (L,c

Mi "/\" Ma is Element of the carrier of (L,c

(minreal || [.L,c

[Mi,Ma] is set

{Mi,Ma} is non empty set

{Mi} is non empty set

{{Mi,Ma},{Mi}} is non empty set

(minreal || [.L,c

[Mi,Ma] is Element of [: the carrier of (L,c

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,c

mi is V31() V32() ext-real Element of REAL

Mi is Element of bool the carrier of (L,c

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

{ b

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

{ b

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,c

L9 is Element of the carrier of (L,c

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,c

(minreal || [.L,c

[ma,L9] is set

{ma,L9} is non empty set

{ma} is non empty set

{{ma,L9},{ma}} is non empty set

(minreal || [.L,c

[ma,L9] is Element of [: the carrier of (L,c

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,c

L9 is V31() V32() ext-real Element of REAL

X is ext-real set

X is Element of the carrier of (L,c

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,c

(minreal || [.L,c

(minreal || [.L,c

(minreal || [.L,c

L9 "/\" X is Element of the carrier of (L,c

z is ext-real Element of ExtREAL

L9 "/\" ma is Element of the carrier of (L,c

(minreal || [.L,c

[L9,ma] is set

{L9,ma} is non empty set

{{L9,ma},{L9}} is non empty set

(minreal || [.L,c

[L9,ma] is Element of [: the carrier of (L,c

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,c

(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

{ b

{0} \/ { b

A is set

{ b

B is V31() V32() ext-real Element of REAL

A is set

B is V31() V32() ext-real Element of REAL

{ b

{ b

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