{} 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
{ b1 where b1 is Element of the carrier of B : a [= b1 } is set
F is Element of the carrier of B
<.F.) is non empty final meet-closed join-closed Element of bool the carrier of B
{ b1 where b1 is Element of the carrier of B : F [= b1 } is 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 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
F1() is non empty set
[:F1(),F1():] is Relation-like non empty set
bool [:F1(),F1():] is non empty set
F2() is Relation-like F1() -defined F1() -valued total V20(F1(),F1()) V29() V31() V36() Element of bool [:F1(),F1():]
bool F1() is non empty set
Class F2() is non empty V26() a_partition of F1()
B is Element of Class F2()
a is set
Class (F2(),a) is Element of bool F1()
F1() is non empty set
[:F1(),F1():] is Relation-like non empty set
bool [:F1(),F1():] is non empty set
F2() is Relation-like F1() -defined F1() -valued total V20(F1(),F1()) V29() V31() V36() Element of bool [:F1(),F1():]
bool F1() is non empty set
Class F2() is non empty V26() a_partition of F1()
B is Element of Class F2()
a is Element of Class F2()
F is set
Class (F2(),F) is Element of bool F1()
E is set
Class (F2(),E) is Element of bool F1()
F1() is non empty set
[:F1(),F1():] is Relation-like non empty set
bool [:F1(),F1():] is non empty set
F2() is Relation-like F1() -defined F1() -valued total V20(F1(),F1()) V29() V31() V36() Element of bool [:F1(),F1():]
bool F1() is non empty set
Class F2() is non empty V26() a_partition of F1()
B is Element of Class F2()
a is Element of Class F2()
F is Element of Class F2()
E is set
Class (F2(),E) is Element of bool F1()
g is set
Class (F2(),g) is Element of bool F1()
S is set
Class (F2(),S) is Element of bool F1()
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) . (H3(S),H3(o1)) is Element of Class a
[(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) . (H3(g),((B,a,E) . (H3(S),H3(o1)))) is Element of Class a
[(EqClass (a,g)),((B,a,E) . (H3(S),H3(o1)))] is set
{(EqClass (a,g)),((B,a,E) . (H3(S),H3(o1)))} is set
{(EqClass (a,g))} is set
{{(EqClass (a,g)),((B,a,E) . (H3(S),H3(o1)))},{(EqClass (a,g))}} is set
(B,a,F) . [(EqClass (a,g)),((B,a,E) . (H3(S),H3(o1)))] is set
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) . (H3(g),H3(E . (S,o1))) is Element of Class a
[(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) . (H3(F . (g,S)),H3(F . (g,o1))) is Element of Class a
[(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) . (H3(g),H3(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)),(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) . (H3(g),H3(S))),H3(F . (g,o1))) is Element of Class a
[((B,a,F) . (H3(g),H3(S))),(EqClass (a,(F . (g,o1))))] is set
{((B,a,F) . (H3(g),H3(S))),(EqClass (a,(F . (g,o1))))} is set
{((B,a,F) . (H3(g),H3(S)))} is set
{{((B,a,F) . (H3(g),H3(S))),(EqClass (a,(F . (g,o1))))},{((B,a,F) . (H3(g),H3(S)))}} is set
(B,a,E) . [((B,a,F) . (H3(g),H3(S))),(EqClass (a,(F . (g,o1))))] is set
(B,a,F) . (H3(g),H3(o1)) is Element of Class a
[(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) . (H3(g),H3(S))),((B,a,F) . (H3(g),H3(o1)))) is Element of Class a
[((B,a,F) . (H3(g),H3(S))),((B,a,F) . (H3(g),H3(o1)))] is set
{((B,a,F) . (H3(g),H3(S))),((B,a,F) . (H3(g),H3(o1)))} is set
{{((B,a,F) . (H3(g),H3(S))),((B,a,F) . (H3(g),H3(o1)))},{((B,a,F) . (H3(g),H3(S)))}} is set
(B,a,E) . [((B,a,F) . (H3(g),H3(S))),((B,a,F) . (H3(g),H3(o1)))] is set
(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) . (H3(g),H3(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,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) . (H3(g),H3(S))),H3(o1)) is Element of Class a
[((B,a,E) . (H3(g),H3(S))),(EqClass (a,o1))] is set
{((B,a,E) . (H3(g),H3(S))),(EqClass (a,o1))} is set
{((B,a,E) . (H3(g),H3(S)))} is set
{{((B,a,E) . (H3(g),H3(S))),(EqClass (a,o1))},{((B,a,E) . (H3(g),H3(S)))}} is set
(B,a,F) . [((B,a,E) . (H3(g),H3(S))),(EqClass (a,o1))] is set
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) . (H3(E . (g,S)),H3(o1)) is Element of Class a
[(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) . (H3(F . (g,o1)),H3(F . (S,o1))) is Element of Class a
[(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) . (H3(g),H3(o1)) is Element of Class a
[(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) . (H3(g),H3(o1))),H3(F . (S,o1))) is Element of Class a
[((B,a,F) . (H3(g),H3(o1))),(EqClass (a,(F . (S,o1))))] is set
{((B,a,F) . (H3(g),H3(o1))),(EqClass (a,(F . (S,o1))))} is set
{((B,a,F) . (H3(g),H3(o1)))} is set
{{((B,a,F) . (H3(g),H3(o1))),(EqClass (a,(F . (S,o1))))},{((B,a,F) . (H3(g),H3(o1)))}} is set
(B,a,E) . [((B,a,F) . (H3(g),H3(o1))),(EqClass (a,(F . (S,o1))))] is set
(B,a,F) . (H3(S),H3(o1)) is Element of Class a
[(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) . (H3(g),H3(o1))),((B,a,F) . (H3(S),H3(o1)))) is Element of Class a
[((B,a,F) . (H3(g),H3(o1))),((B,a,F) . (H3(S),H3(o1)))] is set
{((B,a,F) . (H3(g),H3(o1))),((B,a,F) . (H3(S),H3(o1)))} is set
{{((B,a,F) . (H3(g),H3(o1))),((B,a,F) . (H3(S),H3(o1)))},{((B,a,F) . (H3(g),H3(o1)))}} is set
(B,a,E) . [((B,a,F) . (H3(g),H3(o1))),((B,a,F) . (H3(S),H3(o1)))] is set
(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) . (H3(g),H3(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,E) . [(EqClass (a,g)),(EqClass (a,S))] is set
(B,a,F) . (H3(g),((B,a,E) . (H3(g),H3(S)))) is Element of Class a
[(EqClass (a,g)),((B,a,E) . (H3(g),H3(S)))] is set
{(EqClass (a,g)),((B,a,E) . (H3(g),H3(S)))} is set
{{(EqClass (a,g)),((B,a,E) . (H3(g),H3(S)))},{(EqClass (a,g))}} is set
(B,a,F) . [(EqClass (a,g)),((B,a,E) . (H3(g),H3(S)))] is set
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) . (H3(g),H3(E . (g,S))) is Element of Class a
[(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