:: FILTER_1 semantic presentation

{} is set

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

1 is non empty set

{{},1} is set

K169() is set

bool K169() is non empty set

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

the carrier of B is non empty set

bool the carrier of B is non empty set

a is non empty final meet-closed join-closed Element of bool the carrier of B

F is non empty final meet-closed join-closed Element of bool the carrier of B

a /\ F is Element of bool the carrier of B

E is Element of the carrier of B

g is Element of the carrier of B

E "\/" g is Element of the carrier of B

the L_join of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like non empty total V20([: the carrier of B, the carrier of B:], the carrier of B) commutative associative idempotent Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]

[: the carrier of B, the carrier of B:] is Relation-like non empty set

[:[: the carrier of B, the carrier of B:], the carrier of B:] is Relation-like non empty set

bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty set

the L_join of B . (E,g) is Element of the carrier of B

[E,g] is set

{E,g} is set

{E} is set

{{E,g},{E}} is set

the L_join of B . [E,g] is set

o1 is Element of the carrier of B

o2 is Element of the carrier of B

o1 "/\" o2 is Element of the carrier of B

the L_meet of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like non empty total V20([: the carrier of B, the carrier of B:], the carrier of B) commutative associative idempotent Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]

the L_meet of B . (o1,o2) is Element of the carrier of B

[o1,o2] is set

{o1,o2} is set

{o1} is set

{{o1,o2},{o1}} is set

the L_meet of B . [o1,o2] is set

S is non empty Element of bool the carrier of B

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

the carrier of B is non empty set

a is Element of the carrier of B

<.a.) is non empty final meet-closed join-closed Element of bool the carrier of B

bool the carrier of B is non empty set

{ b

F is Element of the carrier of B

<.F.) is non empty final meet-closed join-closed Element of bool the carrier of B

{ b

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

the carrier of B is non empty set

bool the carrier of B is non empty set

a is non empty final meet-closed join-closed Element of bool the carrier of B

F is non empty final meet-closed join-closed Element of bool the carrier of B

a /\ F is set

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like set

id B is Relation-like B -defined B -valued Function-like one-to-one non empty total V20(B,B) V21(B) V22(B,B) V29() V31() V32() V36() Element of bool [:B,B:]

F is Relation-like B -defined B -valued Function-like non empty total V20(B,B) Element of bool [:B,B:]

E is Element of B

g is Element of B

[E,g] is Element of [:B,B:]

{E,g} is set

{E} is set

{{E,g},{E}} is set

F . E is Element of B

F . g is Element of B

[(F . E),(F . g)] is Element of [:B,B:]

{(F . E),(F . g)} is set

{(F . E)} is set

{{(F . E),(F . g)},{(F . E)}} is set

[:[:B,B:],B:] is Relation-like non empty set

bool [:[:B,B:],B:] is non empty set

pr1 (B,B) is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) Element of bool [:[:B,B:],B:]

F is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) Element of bool [:[:B,B:],B:]

E is Element of B

g is Element of B

[E,g] is Element of [:B,B:]

{E,g} is set

{E} is set

{{E,g},{E}} is set

S is Element of B

o1 is Element of B

[S,o1] is Element of [:B,B:]

{S,o1} is set

{S} is set

{{S,o1},{S}} is set

F . (E,S) is Element of B

[E,S] is set

{E,S} is set

{{E,S},{E}} is set

F . [E,S] is set

F . (g,o1) is Element of B

[g,o1] is set

{g,o1} is set

{g} is set

{{g,o1},{g}} is set

F . [g,o1] is set

[(F . (E,S)),(F . (g,o1))] is Element of [:B,B:]

{(F . (E,S)),(F . (g,o1))} is set

{(F . (E,S))} is set

{{(F . (E,S)),(F . (g,o1))},{(F . (E,S))}} is set

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

F is Relation-like B -defined B -valued Function-like non empty total V20(B,B) Element of bool [:B,B:]

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

[:(Class a),(Class a):] is Relation-like non empty set

bool [:(Class a),(Class a):] is non empty set

E is set

g is set

Class (a,g) is Element of bool B

bool B is non empty set

E is Relation-like Function-like set

dom E is set

rng E is set

g is set

S is set

E . S is set

bool B is non empty set

[:B,(Class a):] is Relation-like non empty set

bool [:B,(Class a):] is non empty set

g is Relation-like B -defined Class a -valued Function-like non empty total V20(B, Class a) Element of bool [:B,(Class a):]

[:(Class a),B:] is Relation-like non empty set

bool [:(Class a),B:] is non empty set

S is Relation-like Class a -defined B -valued Function-like non empty total V20( Class a,B) Element of bool [:(Class a),B:]

g * F is Relation-like B -defined Class a -valued Function-like non empty total V20(B, Class a) Element of bool [:B,(Class a):]

(g * F) * S is Relation-like Class a -defined Class a -valued Function-like non empty total V20( Class a, Class a) Element of bool [:(Class a),(Class a):]

o1 is Relation-like Class a -defined Class a -valued Function-like non empty total V20( Class a, Class a) Element of bool [:(Class a),(Class a):]

o2 is set

o1 . o2 is set

R is set

F . R is set

Class (a,(F . R)) is Element of bool B

dom (g * F) is non empty set

S . o2 is set

rng S is non empty set

(g * F) . (S . o2) is set

F . (S . o2) is set

g . (F . (S . o2)) is set

dom o1 is non empty set

h is Element of Class a

S . h is Element of B

f is Element of B

[(S . h),f] is Element of [:B,B:]

{(S . h),f} is set

{(S . h)} is set

{{(S . h),f},{(S . h)}} is set

x is set

Class (a,x) is Element of bool B

F . (S . h) is Element of B

F . f is Element of B

[(F . (S . h)),(F . f)] is Element of [:B,B:]

{(F . (S . h)),(F . f)} is set

{(F . (S . h))} is set

{{(F . (S . h)),(F . f)},{(F . (S . h))}} is set

EqClass (a,(F . f)) is Element of Class a

g . (F . (S . h)) is Element of Class a

EqClass (a,(F . (S . h))) is Element of Class a

E is Relation-like Class a -defined Class a -valued Function-like non empty total V20( Class a, Class a) Element of bool [:(Class a),(Class a):]

g is Relation-like Class a -defined Class a -valued Function-like non empty total V20( Class a, Class a) Element of bool [:(Class a),(Class a):]

S is set

o1 is set

Class (a,o1) is Element of bool B

bool B is non empty set

E . S is set

F . o1 is set

Class (a,(F . o1)) is Element of bool B

g . S is set

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

[:[:B,B:],B:] is Relation-like non empty set

bool [:[:B,B:],B:] is non empty set

F is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) Element of bool [:[:B,B:],B:]

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

E is set

g is set

Class (a,g) is Element of bool B

bool B is non empty set

E is Relation-like Function-like set

dom E is set

rng E is set

g is set

S is set

E . S is set

bool B is non empty set

[:B,(Class a):] is Relation-like non empty set

bool [:B,(Class a):] is non empty set

g is Relation-like B -defined Class a -valued Function-like non empty total V20(B, Class a) Element of bool [:B,(Class a):]

[:(Class a),B:] is Relation-like non empty set

bool [:(Class a),B:] is non empty set

S is Relation-like Class a -defined B -valued Function-like non empty total V20( Class a,B) Element of bool [:(Class a),B:]

o1 is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

o2 is set

R is set

o1 . (o2,R) is set

[o2,R] is set

{o2,R} is set

{o2} is set

{{o2,R},{o2}} is set

o1 . [o2,R] is set

h is set

f is set

F . (h,f) is set

[h,f] is set

{h,f} is set

{h} is set

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

F . [h,f] is set

Class (a,(F . (h,f))) is Element of bool B

y is Element of Class a

S . y is Element of B

y9 is Element of B

[(S . y),y9] is Element of [:B,B:]

{(S . y),y9} is set

{(S . y)} is set

{{(S . y),y9},{(S . y)}} is set

hx is set

Class (a,hx) is Element of bool B

x is Element of Class a

S . x is Element of B

x9 is Element of B

[(S . x),x9] is Element of [:B,B:]

{(S . x),x9} is set

{(S . x)} is set

{{(S . x),x9},{(S . x)}} is set

hx is set

Class (a,hx) is Element of bool B

F . ((S . x),(S . y)) is Element of B

[(S . x),(S . y)] is set

{(S . x),(S . y)} is set

{{(S . x),(S . y)},{(S . x)}} is set

F . [(S . x),(S . y)] is set

F . (x9,y9) is Element of B

[x9,y9] is set

{x9,y9} is set

{x9} is set

{{x9,y9},{x9}} is set

F . [x9,y9] is set

[(F . ((S . x),(S . y))),(F . (x9,y9))] is Element of [:B,B:]

{(F . ((S . x),(S . y))),(F . (x9,y9))} is set

{(F . ((S . x),(S . y)))} is set

{{(F . ((S . x),(S . y))),(F . (x9,y9))},{(F . ((S . x),(S . y)))}} is set

EqClass (a,(F . (x9,y9))) is Element of Class a

g . (F . ((S . x),(S . y))) is Element of Class a

EqClass (a,(F . ((S . x),(S . y)))) is Element of Class a

o1 . (x,y) is Element of Class a

[x,y] is set

{x,y} is set

{x} is set

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

o1 . [x,y] is set

E is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

g is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

bool B is non empty set

S is Element of Class a

o2 is set

Class (a,o2) is Element of bool B

o1 is Element of Class a

R is set

Class (a,R) is Element of bool B

E . (S,o1) is Element of Class a

[S,o1] is set

{S,o1} is set

{S} is set

{{S,o1},{S}} is set

E . [S,o1] is set

F . (o2,R) is set

[o2,R] is set

{o2,R} is set

{o2} is set

{{o2,R},{o2}} is set

F . [o2,R] is set

Class (a,(F . (o2,R))) is Element of bool B

g . (S,o1) is Element of Class a

g . [S,o1] is set

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

F is Element of B

Class (a,F) is Element of bool B

bool B is non empty set

E is Element of B

Class (a,E) is Element of bool B

g is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,g) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

Class a is non empty V26() a_partition of B

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

(B,a,g) . ((Class (a,F)),(Class (a,E))) is set

[(Class (a,F)),(Class (a,E))] is set

{(Class (a,F)),(Class (a,E))} is set

{(Class (a,F))} is set

{{(Class (a,F)),(Class (a,E))},{(Class (a,F))}} is set

(B,a,g) . [(Class (a,F)),(Class (a,E))] is set

g . (F,E) is Element of B

[F,E] is set

{F,E} is set

{F} is set

{{F,E},{F}} is set

g . [F,E] is set

Class (a,(g . (F,E))) is Element of bool B

EqClass (a,E) is Element of Class a

EqClass (a,F) is Element of Class a

F

[:F

bool [:F

F

bool F

Class F

B is Element of Class F

a is set

Class (F

F

[:F

bool [:F

F

bool F

Class F

B is Element of Class F

a is Element of Class F

F is set

Class (F

E is set

Class (F

F

[:F

bool [:F

F

bool F

Class F

B is Element of Class F

a is Element of Class F

F is Element of Class F

E is set

Class (F

g is set

Class (F

S is set

Class (F

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

F is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,F) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

bool B is non empty set

E is Element of B

EqClass (a,E) is Element of Class a

g is Element of B

EqClass (a,g) is Element of Class a

(B,a,F) . ((EqClass (a,E)),(EqClass (a,g))) is Element of Class a

[(EqClass (a,E)),(EqClass (a,g))] is set

{(EqClass (a,E)),(EqClass (a,g))} is set

{(EqClass (a,E))} is set

{{(EqClass (a,E)),(EqClass (a,g))},{(EqClass (a,E))}} is set

(B,a,F) . [(EqClass (a,E)),(EqClass (a,g))] is set

F . (E,g) is Element of B

[E,g] is set

{E,g} is set

{E} is set

{{E,g},{E}} is set

F . [E,g] is set

Class (a,(F . (E,g))) is Element of bool B

F . (g,E) is Element of B

[g,E] is set

{g,E} is set

{g} is set

{{g,E},{g}} is set

F . [g,E] is set

Class (a,(F . (g,E))) is Element of bool B

(B,a,F) . ((EqClass (a,g)),(EqClass (a,E))) is Element of Class a

[(EqClass (a,g)),(EqClass (a,E))] is set

{(EqClass (a,g)),(EqClass (a,E))} is set

{(EqClass (a,g))} is set

{{(EqClass (a,g)),(EqClass (a,E))},{(EqClass (a,g))}} is set

(B,a,F) . [(EqClass (a,g)),(EqClass (a,E))] is set

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

F is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,F) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

bool B is non empty set

E is Element of B

EqClass (a,E) is Element of Class a

g is Element of B

EqClass (a,g) is Element of Class a

S is Element of B

EqClass (a,S) is Element of Class a

(B,a,F) . ((EqClass (a,g)),(EqClass (a,S))) is Element of Class a

[(EqClass (a,g)),(EqClass (a,S))] is set

{(EqClass (a,g)),(EqClass (a,S))} is set

{(EqClass (a,g))} is set

{{(EqClass (a,g)),(EqClass (a,S))},{(EqClass (a,g))}} is set

(B,a,F) . [(EqClass (a,g)),(EqClass (a,S))] is set

(B,a,F) . ((EqClass (a,E)),((B,a,F) . ((EqClass (a,g)),(EqClass (a,S))))) is Element of Class a

[(EqClass (a,E)),((B,a,F) . ((EqClass (a,g)),(EqClass (a,S))))] is set

{(EqClass (a,E)),((B,a,F) . ((EqClass (a,g)),(EqClass (a,S))))} is set

{(EqClass (a,E))} is set

{{(EqClass (a,E)),((B,a,F) . ((EqClass (a,g)),(EqClass (a,S))))},{(EqClass (a,E))}} is set

(B,a,F) . [(EqClass (a,E)),((B,a,F) . ((EqClass (a,g)),(EqClass (a,S))))] is set

Class (a,E) is Element of bool B

F . (g,S) is Element of B

[g,S] is set

{g,S} is set

{g} is set

{{g,S},{g}} is set

F . [g,S] is set

Class (a,(F . (g,S))) is Element of bool B

(B,a,F) . ((Class (a,E)),(Class (a,(F . (g,S))))) is set

[(Class (a,E)),(Class (a,(F . (g,S))))] is set

{(Class (a,E)),(Class (a,(F . (g,S))))} is set

{(Class (a,E))} is set

{{(Class (a,E)),(Class (a,(F . (g,S))))},{(Class (a,E))}} is set

(B,a,F) . [(Class (a,E)),(Class (a,(F . (g,S))))] is set

F . (E,(F . (g,S))) is Element of B

[E,(F . (g,S))] is set

{E,(F . (g,S))} is set

{E} is set

{{E,(F . (g,S))},{E}} is set

F . [E,(F . (g,S))] is set

Class (a,(F . (E,(F . (g,S))))) is Element of bool B

F . (E,g) is Element of B

[E,g] is set

{E,g} is set

{{E,g},{E}} is set

F . [E,g] is set

F . ((F . (E,g)),S) is Element of B

[(F . (E,g)),S] is set

{(F . (E,g)),S} is set

{(F . (E,g))} is set

{{(F . (E,g)),S},{(F . (E,g))}} is set

F . [(F . (E,g)),S] is set

Class (a,(F . ((F . (E,g)),S))) is Element of bool B

Class (a,(F . (E,g))) is Element of bool B

Class (a,S) is Element of bool B

(B,a,F) . ((Class (a,(F . (E,g)))),(Class (a,S))) is set

[(Class (a,(F . (E,g)))),(Class (a,S))] is set

{(Class (a,(F . (E,g)))),(Class (a,S))} is set

{(Class (a,(F . (E,g))))} is set

{{(Class (a,(F . (E,g)))),(Class (a,S))},{(Class (a,(F . (E,g))))}} is set

(B,a,F) . [(Class (a,(F . (E,g)))),(Class (a,S))] is set

(B,a,F) . ((EqClass (a,E)),(EqClass (a,g))) is Element of Class a

[(EqClass (a,E)),(EqClass (a,g))] is set

{(EqClass (a,E)),(EqClass (a,g))} is set

{{(EqClass (a,E)),(EqClass (a,g))},{(EqClass (a,E))}} is set

(B,a,F) . [(EqClass (a,E)),(EqClass (a,g))] is set

(B,a,F) . (((B,a,F) . ((EqClass (a,E)),(EqClass (a,g)))),(EqClass (a,S))) is Element of Class a

[((B,a,F) . ((EqClass (a,E)),(EqClass (a,g)))),(EqClass (a,S))] is set

{((B,a,F) . ((EqClass (a,E)),(EqClass (a,g)))),(EqClass (a,S))} is set

{((B,a,F) . ((EqClass (a,E)),(EqClass (a,g))))} is set

{{((B,a,F) . ((EqClass (a,E)),(EqClass (a,g)))),(EqClass (a,S))},{((B,a,F) . ((EqClass (a,E)),(EqClass (a,g))))}} is set

(B,a,F) . [((B,a,F) . ((EqClass (a,E)),(EqClass (a,g)))),(EqClass (a,S))] is set

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

F is Element of B

EqClass (a,F) is Element of Class a

bool B is non empty set

E is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,E) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

g is Element of B

EqClass (a,g) is Element of Class a

(B,a,E) . ((EqClass (a,F)),(EqClass (a,g))) is Element of Class a

[(EqClass (a,F)),(EqClass (a,g))] is set

{(EqClass (a,F)),(EqClass (a,g))} is set

{(EqClass (a,F))} is set

{{(EqClass (a,F)),(EqClass (a,g))},{(EqClass (a,F))}} is set

(B,a,E) . [(EqClass (a,F)),(EqClass (a,g))] is set

E . (F,g) is Element of B

[F,g] is set

{F,g} is set

{F} is set

{{F,g},{F}} is set

E . [F,g] is set

Class (a,(E . (F,g))) is Element of bool B

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

F is Element of B

EqClass (a,F) is Element of Class a

bool B is non empty set

E is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,E) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

g is Element of B

EqClass (a,g) is Element of Class a

(B,a,E) . ((EqClass (a,g)),(EqClass (a,F))) is Element of Class a

[(EqClass (a,g)),(EqClass (a,F))] is set

{(EqClass (a,g)),(EqClass (a,F))} is set

{(EqClass (a,g))} is set

{{(EqClass (a,g)),(EqClass (a,F))},{(EqClass (a,g))}} is set

(B,a,E) . [(EqClass (a,g)),(EqClass (a,F))] is set

E . (g,F) is Element of B

[g,F] is set

{g,F} is set

{g} is set

{{g,F},{g}} is set

E . [g,F] is set

EqClass (a,(E . (g,F))) is Element of Class a

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

F is Element of B

EqClass (a,F) is Element of Class a

bool B is non empty set

E is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,E) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

F is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,F) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

E is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,E) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

bool B is non empty set

g is Element of B

EqClass (a,g) is Element of Class a

S is Element of B

EqClass (a,S) is Element of Class a

o1 is Element of B

EqClass (a,o1) is Element of Class a

(B,a,E) . (H

[(EqClass (a,S)),(EqClass (a,o1))] is set

{(EqClass (a,S)),(EqClass (a,o1))} is set

{(EqClass (a,S))} is set

{{(EqClass (a,S)),(EqClass (a,o1))},{(EqClass (a,S))}} is set

(B,a,E) . [(EqClass (a,S)),(EqClass (a,o1))] is set

(B,a,F) . (H

[(EqClass (a,g)),((B,a,E) . (H

{(EqClass (a,g)),((B,a,E) . (H

{(EqClass (a,g))} is set

{{(EqClass (a,g)),((B,a,E) . (H

(B,a,F) . [(EqClass (a,g)),((B,a,E) . (H

E . (S,o1) is Element of B

[S,o1] is set

{S,o1} is set

{S} is set

{{S,o1},{S}} is set

E . [S,o1] is set

EqClass (a,(E . (S,o1))) is Element of Class a

(B,a,F) . (H

[(EqClass (a,g)),(EqClass (a,(E . (S,o1))))] is set

{(EqClass (a,g)),(EqClass (a,(E . (S,o1))))} is set

{{(EqClass (a,g)),(EqClass (a,(E . (S,o1))))},{(EqClass (a,g))}} is set

(B,a,F) . [(EqClass (a,g)),(EqClass (a,(E . (S,o1))))] is set

F . (g,(E . (S,o1))) is Element of B

[g,(E . (S,o1))] is set

{g,(E . (S,o1))} is set

{g} is set

{{g,(E . (S,o1))},{g}} is set

F . [g,(E . (S,o1))] is set

EqClass (a,(F . (g,(E . (S,o1))))) is Element of Class a

F . (g,S) is Element of B

[g,S] is set

{g,S} is set

{{g,S},{g}} is set

F . [g,S] is set

F . (g,o1) is Element of B

[g,o1] is set

{g,o1} is set

{{g,o1},{g}} is set

F . [g,o1] is set

E . ((F . (g,S)),(F . (g,o1))) is Element of B

[(F . (g,S)),(F . (g,o1))] is set

{(F . (g,S)),(F . (g,o1))} is set

{(F . (g,S))} is set

{{(F . (g,S)),(F . (g,o1))},{(F . (g,S))}} is set

E . [(F . (g,S)),(F . (g,o1))] is set

EqClass (a,(E . ((F . (g,S)),(F . (g,o1))))) is Element of Class a

EqClass (a,(F . (g,S))) is Element of Class a

EqClass (a,(F . (g,o1))) is Element of Class a

(B,a,E) . (H

[(EqClass (a,(F . (g,S)))),(EqClass (a,(F . (g,o1))))] is set

{(EqClass (a,(F . (g,S)))),(EqClass (a,(F . (g,o1))))} is set

{(EqClass (a,(F . (g,S))))} is set

{{(EqClass (a,(F . (g,S)))),(EqClass (a,(F . (g,o1))))},{(EqClass (a,(F . (g,S))))}} is set

(B,a,E) . [(EqClass (a,(F . (g,S)))),(EqClass (a,(F . (g,o1))))] is set

(B,a,F) . (H

[(EqClass (a,g)),(EqClass (a,S))] is set

{(EqClass (a,g)),(EqClass (a,S))} is set

{{(EqClass (a,g)),(EqClass (a,S))},{(EqClass (a,g))}} is set

(B,a,F) . [(EqClass (a,g)),(EqClass (a,S))] is set

(B,a,E) . (((B,a,F) . (H

[((B,a,F) . (H

{((B,a,F) . (H

{((B,a,F) . (H

{{((B,a,F) . (H

(B,a,E) . [((B,a,F) . (H

(B,a,F) . (H

[(EqClass (a,g)),(EqClass (a,o1))] is set

{(EqClass (a,g)),(EqClass (a,o1))} is set

{{(EqClass (a,g)),(EqClass (a,o1))},{(EqClass (a,g))}} is set

(B,a,F) . [(EqClass (a,g)),(EqClass (a,o1))] is set

(B,a,E) . (((B,a,F) . (H

[((B,a,F) . (H

{((B,a,F) . (H

{{((B,a,F) . (H

(B,a,E) . [((B,a,F) . (H

(B,a,E) . ((EqClass (a,S)),(EqClass (a,o1))) is Element of Class a

(B,a,F) . ((EqClass (a,g)),((B,a,E) . ((EqClass (a,S)),(EqClass (a,o1))))) is Element of Class a

[(EqClass (a,g)),((B,a,E) . ((EqClass (a,S)),(EqClass (a,o1))))] is set

{(EqClass (a,g)),((B,a,E) . ((EqClass (a,S)),(EqClass (a,o1))))} is set

{{(EqClass (a,g)),((B,a,E) . ((EqClass (a,S)),(EqClass (a,o1))))},{(EqClass (a,g))}} is set

(B,a,F) . [(EqClass (a,g)),((B,a,E) . ((EqClass (a,S)),(EqClass (a,o1))))] is set

(B,a,F) . ((EqClass (a,g)),(EqClass (a,S))) is Element of Class a

(B,a,F) . ((EqClass (a,g)),(EqClass (a,o1))) is Element of Class a

(B,a,E) . (((B,a,F) . ((EqClass (a,g)),(EqClass (a,S)))),((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1))))) is Element of Class a

[((B,a,F) . ((EqClass (a,g)),(EqClass (a,S)))),((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1))))] is set

{((B,a,F) . ((EqClass (a,g)),(EqClass (a,S)))),((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1))))} is set

{((B,a,F) . ((EqClass (a,g)),(EqClass (a,S))))} is set

{{((B,a,F) . ((EqClass (a,g)),(EqClass (a,S)))),((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1))))},{((B,a,F) . ((EqClass (a,g)),(EqClass (a,S))))}} is set

(B,a,E) . [((B,a,F) . ((EqClass (a,g)),(EqClass (a,S)))),((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1))))] is set

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

F is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,F) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

E is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,E) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

bool B is non empty set

g is Element of B

EqClass (a,g) is Element of Class a

S is Element of B

EqClass (a,S) is Element of Class a

(B,a,E) . (H

[(EqClass (a,g)),(EqClass (a,S))] is set

{(EqClass (a,g)),(EqClass (a,S))} is set

{(EqClass (a,g))} is set

{{(EqClass (a,g)),(EqClass (a,S))},{(EqClass (a,g))}} is set

(B,a,E) . [(EqClass (a,g)),(EqClass (a,S))] is set

o1 is Element of B

EqClass (a,o1) is Element of Class a

(B,a,F) . (((B,a,E) . (H

[((B,a,E) . (H

{((B,a,E) . (H

{((B,a,E) . (H

{{((B,a,E) . (H

(B,a,F) . [((B,a,E) . (H

E . (g,S) is Element of B

[g,S] is set

{g,S} is set

{g} is set

{{g,S},{g}} is set

E . [g,S] is set

EqClass (a,(E . (g,S))) is Element of Class a

(B,a,F) . (H

[(EqClass (a,(E . (g,S)))),(EqClass (a,o1))] is set

{(EqClass (a,(E . (g,S)))),(EqClass (a,o1))} is set

{(EqClass (a,(E . (g,S))))} is set

{{(EqClass (a,(E . (g,S)))),(EqClass (a,o1))},{(EqClass (a,(E . (g,S))))}} is set

(B,a,F) . [(EqClass (a,(E . (g,S)))),(EqClass (a,o1))] is set

F . ((E . (g,S)),o1) is Element of B

[(E . (g,S)),o1] is set

{(E . (g,S)),o1} is set

{(E . (g,S))} is set

{{(E . (g,S)),o1},{(E . (g,S))}} is set

F . [(E . (g,S)),o1] is set

EqClass (a,(F . ((E . (g,S)),o1))) is Element of Class a

F . (g,o1) is Element of B

[g,o1] is set

{g,o1} is set

{{g,o1},{g}} is set

F . [g,o1] is set

F . (S,o1) is Element of B

[S,o1] is set

{S,o1} is set

{S} is set

{{S,o1},{S}} is set

F . [S,o1] is set

E . ((F . (g,o1)),(F . (S,o1))) is Element of B

[(F . (g,o1)),(F . (S,o1))] is set

{(F . (g,o1)),(F . (S,o1))} is set

{(F . (g,o1))} is set

{{(F . (g,o1)),(F . (S,o1))},{(F . (g,o1))}} is set

E . [(F . (g,o1)),(F . (S,o1))] is set

EqClass (a,(E . ((F . (g,o1)),(F . (S,o1))))) is Element of Class a

EqClass (a,(F . (g,o1))) is Element of Class a

EqClass (a,(F . (S,o1))) is Element of Class a

(B,a,E) . (H

[(EqClass (a,(F . (g,o1)))),(EqClass (a,(F . (S,o1))))] is set

{(EqClass (a,(F . (g,o1)))),(EqClass (a,(F . (S,o1))))} is set

{(EqClass (a,(F . (g,o1))))} is set

{{(EqClass (a,(F . (g,o1)))),(EqClass (a,(F . (S,o1))))},{(EqClass (a,(F . (g,o1))))}} is set

(B,a,E) . [(EqClass (a,(F . (g,o1)))),(EqClass (a,(F . (S,o1))))] is set

(B,a,F) . (H

[(EqClass (a,g)),(EqClass (a,o1))] is set

{(EqClass (a,g)),(EqClass (a,o1))} is set

{{(EqClass (a,g)),(EqClass (a,o1))},{(EqClass (a,g))}} is set

(B,a,F) . [(EqClass (a,g)),(EqClass (a,o1))] is set

(B,a,E) . (((B,a,F) . (H

[((B,a,F) . (H

{((B,a,F) . (H

{((B,a,F) . (H

{{((B,a,F) . (H

(B,a,E) . [((B,a,F) . (H

(B,a,F) . (H

[(EqClass (a,S)),(EqClass (a,o1))] is set

{(EqClass (a,S)),(EqClass (a,o1))} is set

{(EqClass (a,S))} is set

{{(EqClass (a,S)),(EqClass (a,o1))},{(EqClass (a,S))}} is set

(B,a,F) . [(EqClass (a,S)),(EqClass (a,o1))] is set

(B,a,E) . (((B,a,F) . (H

[((B,a,F) . (H

{((B,a,F) . (H

{{((B,a,F) . (H

(B,a,E) . [((B,a,F) . (H

(B,a,E) . ((EqClass (a,g)),(EqClass (a,S))) is Element of Class a

(B,a,F) . (((B,a,E) . ((EqClass (a,g)),(EqClass (a,S)))),(EqClass (a,o1))) is Element of Class a

[((B,a,E) . ((EqClass (a,g)),(EqClass (a,S)))),(EqClass (a,o1))] is set

{((B,a,E) . ((EqClass (a,g)),(EqClass (a,S)))),(EqClass (a,o1))} is set

{((B,a,E) . ((EqClass (a,g)),(EqClass (a,S))))} is set

{{((B,a,E) . ((EqClass (a,g)),(EqClass (a,S)))),(EqClass (a,o1))},{((B,a,E) . ((EqClass (a,g)),(EqClass (a,S))))}} is set

(B,a,F) . [((B,a,E) . ((EqClass (a,g)),(EqClass (a,S)))),(EqClass (a,o1))] is set

(B,a,F) . ((EqClass (a,g)),(EqClass (a,o1))) is Element of Class a

(B,a,F) . ((EqClass (a,S)),(EqClass (a,o1))) is Element of Class a

(B,a,E) . (((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1)))),((B,a,F) . ((EqClass (a,S)),(EqClass (a,o1))))) is Element of Class a

[((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1)))),((B,a,F) . ((EqClass (a,S)),(EqClass (a,o1))))] is set

{((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1)))),((B,a,F) . ((EqClass (a,S)),(EqClass (a,o1))))} is set

{((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1))))} is set

{{((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1)))),((B,a,F) . ((EqClass (a,S)),(EqClass (a,o1))))},{((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1))))}} is set

(B,a,E) . [((B,a,F) . ((EqClass (a,g)),(EqClass (a,o1)))),((B,a,F) . ((EqClass (a,S)),(EqClass (a,o1))))] is set

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

F is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,F) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

E is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,E) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

B is non empty set

[:B,B:] is Relation-like non empty set

bool [:B,B:] is non empty set

a is Relation-like B -defined B -valued total V20(B,B) V29() V31() V36() Element of bool [:B,B:]

Class a is non empty V26() a_partition of B

F is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,F) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

[:(Class a),(Class a):] is Relation-like non empty set

[:[:(Class a),(Class a):],(Class a):] is Relation-like non empty set

bool [:[:(Class a),(Class a):],(Class a):] is non empty set

E is Relation-like [:B,B:] -defined B -valued Function-like non empty total V20([:B,B:],B) (B,a)

(B,a,E) is Relation-like [:(Class a),(Class a):] -defined Class a -valued Function-like non empty total V20([:(Class a),(Class a):], Class a) Element of bool [:[:(Class a),(Class a):],(Class a):]

bool B is non empty set

g is Element of B

EqClass (a,g) is Element of Class a

S is Element of B

EqClass (a,S) is Element of Class a

(B,a,E) . (H

[(EqClass (a,g)),(EqClass (a,S))] is set

{(EqClass (a,g)),(EqClass (a,S))} is set

{(EqClass (a,g))} is set

{{(EqClass (a,g)),(EqClass (a,S))},{(EqClass (a,g))}} is set

(B,a,E) . [(EqClass (a,g)),(EqClass (a,S))] is set

(B,a,F) . (H

[(EqClass (a,g)),((B,a,E) . (H

{(EqClass (a,g)),((B,a,E) . (H

{{(EqClass (a,g)),((B,a,E) . (H

(B,a,F) . [(EqClass (a,g)),((B,a,E) . (H

E . (g,S) is Element of B

[g,S] is set

{g,S} is set

{g} is set

{{g,S},{g}} is set

E . [g,S] is set

EqClass (a,(E . (g,S))) is Element of Class a

(B,a,F) . (H

[(EqClass (a,g)),(EqClass (a,(E . (g,S))))] is set

{(EqClass (a,g)),(EqClass (a,(E . (g,S))))} is set

{{(EqClass (a,g)),(EqClass (a,(E . (g,S))))},{(EqClass (a,g))}} is set

(B,a,F) . [(EqClass (a,g)),(EqClass (a,(E . (g,S))))] is set

F . (g,(E . (g,S))) is Element of B

[g,(E . (g,S))] is set

{g,(E . (g,S))} is set

{{g,(E . (g,S))},{g}} is set

F . [g,(E . (g,S))] is set

EqClass (a,(F . (g,(E . (g,S))))) is Element of Class a

(B,a,E) . ((EqClass (a,g)),(EqClass (a,S))) is Element of Class a

(B,a,F) . ((EqClass (a,g)),((B,a,E) . ((EqClass (a,g)),(EqClass (a,S))))) is Element of Class a

[(EqClass (a,g)),((B,a,E) . ((EqClass (a,g)),(EqClass (a,S))))] is set

{(EqClass (a,g)),((B,a,E) . ((EqClass (a,g)),(EqClass (a,S))))} is set

{{(EqClass (a,g)),((B,a,E) . ((EqClass (a,g)),(EqClass (a,S))))},{(EqClass (a,g))}} is set

(B,a,F) . [(EqClass (a,g)),((B,a,E) . ((EqClass (a,g)),(EqClass (a,S))))] is set

B is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative LattStr

the carrier of B is non empty set

bool the carrier of B is non empty set

the L_join of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like non empty total V20([: the carrier of B, the carrier of B:], the carrier of B) commutative associative idempotent Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]

[: the carrier of B, the carrier of B:] is Relation-like non empty set

[:[: the carrier of B, the carrier of B:], the carrier of B:] is Relation-like non empty set

bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty set

a is non empty final meet-closed join-closed Element of bool the carrier of B

equivalence_wrt a is Relation-like the carrier of B -defined the carrier of B -valued total V20( the carrier of B, the carrier of B) V29() V31() V36() Element of bool [: the carrier of B, the carrier of B:]

bool [: the carrier of B, the carrier of B:] is non empty set

E is Element of the carrier of B

g is Element of the carrier of B

[E,g] is Element of [: the carrier of B, the carrier of B:]

{E,g} is set

{E} is set

{{E,g},{E}} is set

S is Element of the carrier of B

o1 is Element of the carrier of B

[S,o1] is Element of [: the carrier of B, the carrier of B:]

{S,o1} is set

{S} is set

{{S,o1},{S}} is set

the L_join of B . (E,S) is Element of the carrier of B

[E,S] is set

{E,S} is set

{{E,S},{E}} is set

the L_join of B . [E,S] is set

the L_join of B . (g,o1) is Element of the carrier of B

[g,o1] is set

{g,o1} is set

{g} is set

{{g,o1},{g}} is set

the L_join of B . [g,o1] is set

[( the L_join of B . (E,S)),( the L_join of B . (g,o1))] is Element of [: the carrier of B, the carrier of B:]

{( the L_join of B . (E,S)),( the L_join of B . (g,o1))} is set

{( the L_join of B . (E,S))} is set

{{( the L_join of B . (E,S)),( the L_join of B . (g,o1))},{( the L_join of B . (E,S))}} is set

S <=> o1 is Element of the carrier of B

S => o1 is Element of the carrier of B

o1 => S is Element of the carrier of B

(S => o1) "/\" (o1 => S) is Element of the carrier of B

the L_meet of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like non empty total V20([: the carrier of B, the carrier of B:], the carrier of B) commutative associative idempotent Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]

the L_meet of B . ((S => o1),(o1 => S)) is Element of the carrier of B

[(S => o1),(o1 => S)] is set

{(S => o1),(o1 => S)} is set

{(S => o1)} is set

{{(S => o1),(o1 => S)},{(S => o1)}} is set

the L_meet of B . [(S => o1),(o1 => S)] is set

E => g is Element of the carrier of B

E "/\" (E => g) is Element of the carrier of B

the L_meet of B . (E,(E => g)) is Element of the carrier of B

[E,(E => g)] is set

{E,(E => g)} is set

{{E,(E => g)},{E}} is set

the L_meet of B . [E,(E => g)] is set

(E => g) "/\" (S => o1) is Element of the carrier of B

the L_meet of B . ((E => g),(S => o1)) is Element of the carrier of B

[(E => g),(S => o1)] is set

{(E => g),(S => o1)} is set

{(E => g)} is set

{{(E => g),(S => o1)},{(E => g)}} is set

the L_meet of B . [(E => g),(S => o1)] is set

E "/\" ((E => g) "/\" (S => o1)) is Element of the carrier of B

the L_meet of B . (E,((E => g) "/\" (S => o1))) is Element of the carrier of B

[E,((E => g) "/\" (S => o1))] is set

{E,((E => g) "/\" (S => o1))} is set

{{E,((E => g) "/\" (S => o1))},{E}} is set

the L_meet of B . [E,((E => g) "/\" (S => o1))] is set

(E "/\" (E => g)) "/\" (S => o1) is Element of the carrier of B

the L_meet of B . ((E "/\" (E => g)),(S => o1)) is Element of the carrier of B

[(E "/\" (E => g)),(S => o1)] is set

{(E "/\" (E => g)),(S => o1)} is set

{(E "/\" (E => g))} is set

{{(E "/\" (E => g)),(S => o1)},{(E "/\" (E => g))}} is set

the L_meet of B . [(E "/\" (E => g)),(S => o1)] is set

S "/\" ((E => g) "/\" (S => o1)) is Element of the carrier of B

the L_meet of B . (S,((E => g) "/\" (S => o1))) is Element of the carrier of B

[S,((E => g) "/\" (S => o1))] is set

{S,((E => g) "/\" (S => o1))} is set

{{S,((E => g) "/\" (S => o1))},{S}} is set

the L_meet of B . [S,((E => g) "/\" (S => o1))] is set

S "/\" (E => g) is Element of the carrier of B

the L_meet of B . (S,(E => g)) is Element of the carrier of B

[S,(E => g)] is set

{S,(E => g)} is set

{{S,(E => g)},{S}} is set

the L_meet of B . [S,(E => g)] is set

(S "/\" (E => g)) "/\" (S => o1) is Element of the carrier of B

the L_meet of B . ((S "/\" (E => g)),(S => o1)) is Element of the carrier of B

[(S "/\" (E => g)),(S => o1)] is set

{(S "/\" (E => g)),(S => o1)} is set

{(S "/\" (E => g))} is set

{{(S "/\" (E => g)),(S => o1)},{(S "/\" (E => g))}} is set

the L_meet of B . [(S "/\" (E => g)),(S => o1)] is set

S "/\" (S => o1) is Element of the carrier of B

the L_meet of B . (S,(S => o1)) is Element of the carrier of B

[S,(S => o1)] is set

{S,(S => o1)} is set

{{S,(S => o1)},{S}} is set

the L_meet of B . [S,(S => o1)] is set

(E => g) "/\" (S "/\" (S => o1)) is Element of the carrier of B

the L_meet of B . ((E => g),(S "/\" (S => o1))) is Element of the carrier of B

[(E => g),(S "/\" (S => o1))] is set

{(E => g),(S "/\" (S => o1))} is set

{{(E => g),(S "/\" (S => o1))},{(E => g)}} is set

the L_meet of B . [(E => g),(S "/\" (S => o1))] is set

(E => g) "/\" S is Element of the carrier of B

the L_meet of B . ((E => g),S) is Element of the carrier of B

[(E => g),S] is set

{(E => g),S} is set

{{(E => g),S},{(E => g)}} is set

the L_meet of B . [(E => g),S] is set

((E => g) "/\" S) "/\" (S => o1) is Element of the carrier of B

the L_meet of B . (((E => g) "/\" S),(S => o1)) is Element of the carrier of B

[((E => g) "/\" S),(S => o1)] is set

{((E => g) "/\" S),(S => o1)} is set

{((E => g) "/\" S)} is set

{{((E => g) "/\" S),(S => o1)},{((E => g) "/\" S)}} is set

the L_meet of B . [((E => g) "/\" S),(S => o1)] is set

(E "/\" ((E => g) "/\" (S => o1))) "\/" (S "/\" ((E => g) "/\" (S => o1))) is Element of the carrier of B

the L_join of B . ((E "/\" ((E => g) "/\" (S => o1))),(S "/\" ((E => g) "/\" (S => o1)))) is Element of the carrier of B

[(E "/\" ((E => g) "/\" (S => o1))),(S "/\" ((E => g) "/\" (S => o1)))] is set

{(E "/\" ((E => g) "/\" (S => o1))),(S "/\" ((E => g) "/\" (S => o1)))} is set

{(E "/\" ((E => g) "/\" (S => o1)))} is set

{{(E "/\" ((E => g) "/\" (S => o1))),(S "/\" ((E => g) "/\" (S => o1)))},{(E "/\" ((E => g) "/\" (S => o1)))}} is set

the L_join of B . [(E "/\" ((E => g) "/\" (S => o1))),(S "/\" ((E => g) "/\" (S => o1)))] is set

g "\/" o1 is Element of the carrier of B

E "\/" S is Element of the carrier of B

(E "\/" S) "/\" ((E => g) "/\" (S => o1)) is Element of the carrier of B

the L_meet of B . ((E "\/" S),((E => g) "/\" (S => o1))) is Element of the carrier of B

[(E "\/" S),((E => g) "/\" (S => o1))] is set

{(E "\/" S),((E => g) "/\" (S => o1))} is set

{(E "\/" S)} is set

{{(E "\/" S),((E => g) "/\" (S => o1))},{(E "\/" S)}} is set

the L_meet of B . [(E "\/" S),((E => g) "/\" (S => o1))] is set

(E "\/" S) => (g "\/" o1) is Element of the carrier of B

g => E is Element of the carrier of B

g "/\" (g => E) is Element of the carrier of B

the L_meet of B . (g,(g => E)) is Element of the carrier of B

[g,(g => E)] is set

{g,(g => E)} is set

{{g,(g => E)},{g}} is set

the L_meet of B . [g,(g => E)] is set

(g => E) "/\" (o1 => S) is Element of the carrier of B

the L_meet of B . ((g => E),(o1 => S)) is Element of the carrier of B

[(g => E),(o1 => S)] is set

{(g => E),(o1 => S)} is set

{(g => E)} is set

{{(g => E),(o1 => S)},{(g => E)}} is set

the L_meet of B . [(g => E),(o1 => S)] is set

g "/\" ((g => E) "/\" (o1 => S)) is Element of the carrier of B

the L_meet of B . (g,((g => E) "/\" (o1 => S))) is Element of the carrier of B

[g,((g => E) "/\" (o1 => S))] is set

{g,((g => E) "/\" (o1 => S))} is set

{{g,((g => E) "/\" (o1 => S))},{g}} is set

the L_meet of B . [g,((g => E) "/\" (o1 => S))] is set

(g "/\" (g => E)) "/\" (o1 => S) is Element of the carrier of B

the L_meet of B . ((g "/\" (g => E)),(o1