K110() is set
K114() is non empty V21() V22() V23() V28() cardinal limit_cardinal Element of bool K110()
bool K110() is non empty set
K87() is non empty V21() V22() V23() V28() cardinal limit_cardinal set
bool K87() is non empty V28() set
K234() is non empty strict TopSpace-like T_0 T_1 T_2 compact TopStruct
the carrier of K234() is non empty set
bool K114() is non empty V28() set
{} is empty Function-like functional V21() V22() V23() V25() V26() V27() V28() cardinal {} -element set
the empty Function-like functional V21() V22() V23() V25() V26() V27() V28() cardinal {} -element set is empty Function-like functional V21() V22() V23() V25() V26() V27() V28() cardinal {} -element set
1 is non empty V21() V22() V23() V27() V28() cardinal Element of K114()
{{},1} is non empty set
id {} is Relation-like Function-like one-to-one set
G is set
[:G,G:] is set
bool [:G,G:] is non empty set
id G is Relation-like G -defined G -valued Function-like one-to-one V14(G) quasi_total Element of bool [:G,G:]
rng (id G) is Element of bool G
bool G is non empty set
G is 1-sorted
the carrier of G is set
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
rng (id G) is Element of bool the carrier of G
bool the carrier of G is non empty set
[#] G is non proper Element of bool the carrier of G
G is 1-sorted
the carrier of G is set
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(id G) /" is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
rng (id G) is Element of bool the carrier of G
bool the carrier of G is non empty set
[#] G is non proper Element of bool the carrier of G
G is 1-sorted
the carrier of G is set
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(id G) /" is Relation-like the carrier of G -defined the carrier of G -defined the carrier of G -valued the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total quasi_total Element of bool [: the carrier of G, the carrier of G:]
rng (id G) is Element of bool the carrier of G
bool the carrier of G is non empty set
[#] G is non proper Element of bool the carrier of G
(id the carrier of G) " is Relation-like Function-like one-to-one set
G is 1-sorted
the carrier of G is set
bool the carrier of G is non empty set
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
e is Element of bool the carrier of G
(id G) " e is Element of bool the carrier of G
rng (id G) is Element of bool the carrier of G
[#] G is non proper Element of bool the carrier of G
(id G) .: e is Element of bool the carrier of G
(id G) /" is Relation-like the carrier of G -defined the carrier of G -defined the carrier of G -valued the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total quasi_total Element of bool [: the carrier of G, the carrier of G:]
((id G) /") " e is Element of bool the carrier of G
G is non empty multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
e is Element of bool the carrier of G
A is Element of bool the carrier of G
C is Element of bool the carrier of G
e * C is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in e & b2 in C ) } is set
B is Element of bool the carrier of G
A * B is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in A & b2 in B ) } is set
W is set
p is Element of the carrier of G
r is Element of the carrier of G
p * r is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (p,r) is Element of the carrier of G
[p,r] is set
{p,r} is non empty set
{p} is non empty trivial 1 -element set
{{p,r},{p}} is non empty set
the multF of G . [p,r] is set
G is non empty multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
e is Element of bool the carrier of G
A is Element of bool the carrier of G
C is Element of the carrier of G
e * C is Element of bool the carrier of G
{C} is non empty trivial 1 -element Element of bool the carrier of G
e * {C} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in e & b2 in {C} ) } is set
A * C is Element of bool the carrier of G
A * {C} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in A & b2 in {C} ) } is set
B is set
W is Element of the carrier of G
W * C is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (W,C) is Element of the carrier of G
[W,C] is set
{W,C} is non empty set
{W} is non empty trivial 1 -element set
{{W,C},{W}} is non empty set
the multF of G . [W,C] is set
G is non empty multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
e is Element of bool the carrier of G
A is Element of bool the carrier of G
C is Element of the carrier of G
C * e is Element of bool the carrier of G
{C} is non empty trivial 1 -element Element of bool the carrier of G
{C} * e is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {C} & b2 in e ) } is set
C * A is Element of bool the carrier of G
{C} * A is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {C} & b2 in A ) } is set
B is set
W is Element of the carrier of G
C * W is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (C,W) is Element of the carrier of G
[C,W] is set
{C,W} is non empty set
{C} is non empty trivial 1 -element set
{{C,W},{C}} is non empty set
the multF of G . [C,W] is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
e is Element of bool the carrier of G
e " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in e } is set
A is Element of the carrier of G
A " is Element of the carrier of G
(A ") " is Element of the carrier of G
(e ") " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in e " } is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
e is Element of bool the carrier of G
e " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in e } is set
A is Element of bool the carrier of G
A " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in A } is set
C is set
B is Element of the carrier of G
B " is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
e is Element of bool the carrier of G
e " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in e } is set
A is Element of bool the carrier of G
A " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in A } is set
(e ") " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in e " } is set
(A ") " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in A " } is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
inverse_op G is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
e is Element of bool the carrier of G
(inverse_op G) .: e is Element of bool the carrier of G
e " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in e } is set
C is set
B is set
(inverse_op G) . B is set
W is Element of the carrier of G
W " is Element of the carrier of G
C is set
B is Element of the carrier of G
B " is Element of the carrier of G
(inverse_op G) . B is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
inverse_op G is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
e is Element of bool the carrier of G
(inverse_op G) " e is Element of bool the carrier of G
e " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in e } is set
dom (inverse_op G) is Element of bool the carrier of G
C is set
(inverse_op G) . C is set
B is Element of the carrier of G
(inverse_op G) . B is Element of the carrier of G
((inverse_op G) . B) " is Element of the carrier of G
B " is Element of the carrier of G
(B ") " is Element of the carrier of G
C is set
B is Element of the carrier of G
B " is Element of the carrier of G
(inverse_op G) . (B ") is Element of the carrier of G
(B ") " is Element of the carrier of G
G is non empty unital Group-like associative multMagma
inverse_op G is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
A is set
dom (inverse_op G) is set
C is set
(inverse_op G) . A is set
(inverse_op G) . C is set
dom (inverse_op G) is Element of bool the carrier of G
bool the carrier of G is non empty set
B is Element of the carrier of G
(inverse_op G) . B is Element of the carrier of G
B " is Element of the carrier of G
W is Element of the carrier of G
(inverse_op G) . W is Element of the carrier of G
W " is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
inverse_op G is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
rng (inverse_op G) is Element of bool the carrier of G
bool the carrier of G is non empty set
A is set
dom (inverse_op G) is Element of bool the carrier of G
C is Element of the carrier of G
C " is Element of the carrier of G
(inverse_op G) . (C ") is Element of the carrier of G
(C ") " is Element of the carrier of G
G is non empty unital Group-like associative multMagma
inverse_op G is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
rng (inverse_op G) is Element of bool the carrier of G
bool the carrier of G is non empty set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
inverse_op G is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total onto bijective Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
(inverse_op G) " is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total onto bijective Element of bool [: the carrier of G, the carrier of G:]
dom (inverse_op G) is Element of bool the carrier of G
bool the carrier of G is non empty set
A is set
C is Element of the carrier of G
C " is Element of the carrier of G
(inverse_op G) . (C ") is Element of the carrier of G
(C ") " is Element of the carrier of G
(inverse_op G) . A is set
((inverse_op G) ") . A is set
dom ((inverse_op G) ") is Element of bool the carrier of G
G is non empty multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is non empty set
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
e is Element of bool the carrier of G
A is Element of bool the carrier of G
[:e,A:] is set
the multF of G .: [:e,A:] is Element of bool the carrier of G
e * A is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in e & b2 in A ) } is set
B is set
W is set
the multF of G . W is set
p is set
r is set
[p,r] is set
{p,r} is non empty set
{p} is non empty trivial 1 -element set
{{p,r},{p}} is non empty set
a is Element of the carrier of G
a is Element of the carrier of G
a * a is Element of the carrier of G
the multF of G . (a,a) is Element of the carrier of G
[a,a] is set
{a,a} is non empty set
{a} is non empty trivial 1 -element set
{{a,a},{a}} is non empty set
the multF of G . [a,a] is set
B is set
W is Element of the carrier of G
p is Element of the carrier of G
W * p is Element of the carrier of G
the multF of G . (W,p) is Element of the carrier of G
[W,p] is set
{W,p} is non empty set
{W} is non empty trivial 1 -element set
{{W,p},{W}} is non empty set
the multF of G . [W,p] is set
[W,p] is Element of [: the carrier of G, the carrier of G:]
G is non empty multMagma
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
e is Element of the carrier of G
A is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
C is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
B is Element of the carrier of G
C . B is Element of the carrier of G
e * B is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (e,B) is Element of the carrier of G
[e,B] is set
{e,B} is non empty set
{e} is non empty trivial 1 -element set
{{e,B},{e}} is non empty set
the multF of G . [e,B] is set
A is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
C is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
B is set
A . B is set
W is Element of the carrier of G
e * W is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (e,W) is Element of the carrier of G
[e,W] is set
{e,W} is non empty set
{e} is non empty trivial 1 -element set
{{e,W},{e}} is non empty set
the multF of G . [e,W] is set
C . B is set
A is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
C is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
B is Element of the carrier of G
C . B is Element of the carrier of G
B * e is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (B,e) is Element of the carrier of G
[B,e] is set
{B,e} is non empty set
{B} is non empty trivial 1 -element set
{{B,e},{B}} is non empty set
the multF of G . [B,e] is set
A is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
C is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
B is set
A . B is set
W is Element of the carrier of G
W * e is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (W,e) is Element of the carrier of G
[W,e] is set
{W,e} is non empty set
{W} is non empty trivial 1 -element set
{{W,e},{W}} is non empty set
the multF of G . [W,e] is set
C . B is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
e is Element of the carrier of G
(G,e) is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
dom (G,e) is Element of bool the carrier of G
bool the carrier of G is non empty set
C is set
B is set
(G,e) . C is set
(G,e) . B is set
W is Element of the carrier of G
(G,e) . W is Element of the carrier of G
e * W is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (e,W) is Element of the carrier of G
[e,W] is set
{e,W} is non empty set
{e} is non empty trivial 1 -element set
{{e,W},{e}} is non empty set
the multF of G . [e,W] is set
p is Element of the carrier of G
(G,e) . p is Element of the carrier of G
e * p is Element of the carrier of G
the multF of G . (e,p) is Element of the carrier of G
[e,p] is set
{e,p} is non empty set
{{e,p},{e}} is non empty set
the multF of G . [e,p] is set
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * W is Element of the carrier of G
the multF of G . ((1_ G),W) is Element of the carrier of G
[(1_ G),W] is set
{(1_ G),W} is non empty set
{(1_ G)} is non empty trivial 1 -element set
{{(1_ G),W},{(1_ G)}} is non empty set
the multF of G . [(1_ G),W] is set
e " is Element of the carrier of G
(e ") * e is Element of the carrier of G
the multF of G . ((e "),e) is Element of the carrier of G
[(e "),e] is set
{(e "),e} is non empty set
{(e ")} is non empty trivial 1 -element set
{{(e "),e},{(e ")}} is non empty set
the multF of G . [(e "),e] is set
((e ") * e) * W is Element of the carrier of G
the multF of G . (((e ") * e),W) is Element of the carrier of G
[((e ") * e),W] is set
{((e ") * e),W} is non empty set
{((e ") * e)} is non empty trivial 1 -element set
{{((e ") * e),W},{((e ") * e)}} is non empty set
the multF of G . [((e ") * e),W] is set
(e ") * (e * W) is Element of the carrier of G
the multF of G . ((e "),(e * W)) is Element of the carrier of G
[(e "),(e * W)] is set
{(e "),(e * W)} is non empty set
{{(e "),(e * W)},{(e ")}} is non empty set
the multF of G . [(e "),(e * W)] is set
((e ") * e) * p is Element of the carrier of G
the multF of G . (((e ") * e),p) is Element of the carrier of G
[((e ") * e),p] is set
{((e ") * e),p} is non empty set
{{((e ") * e),p},{((e ") * e)}} is non empty set
the multF of G . [((e ") * e),p] is set
(1_ G) * p is Element of the carrier of G
the multF of G . ((1_ G),p) is Element of the carrier of G
[(1_ G),p] is set
{(1_ G),p} is non empty set
{{(1_ G),p},{(1_ G)}} is non empty set
the multF of G . [(1_ G),p] is set
rng (G,e) is Element of bool the carrier of G
C is set
B is Element of the carrier of G
(e ") * B is Element of the carrier of G
the multF of G . ((e "),B) is Element of the carrier of G
[(e "),B] is set
{(e "),B} is non empty set
{{(e "),B},{(e ")}} is non empty set
the multF of G . [(e "),B] is set
(G,e) . ((e ") * B) is Element of the carrier of G
e * ((e ") * B) is Element of the carrier of G
the multF of G . (e,((e ") * B)) is Element of the carrier of G
[e,((e ") * B)] is set
{e,((e ") * B)} is non empty set
{{e,((e ") * B)},{e}} is non empty set
the multF of G . [e,((e ") * B)] is set
e * (e ") is Element of the carrier of G
the multF of G . (e,(e ")) is Element of the carrier of G
[e,(e ")] is set
{e,(e ")} is non empty set
{{e,(e ")},{e}} is non empty set
the multF of G . [e,(e ")] is set
(e * (e ")) * B is Element of the carrier of G
the multF of G . ((e * (e ")),B) is Element of the carrier of G
[(e * (e ")),B] is set
{(e * (e ")),B} is non empty set
{(e * (e "))} is non empty trivial 1 -element set
{{(e * (e ")),B},{(e * (e "))}} is non empty set
the multF of G . [(e * (e ")),B] is set
(1_ G) * B is Element of the carrier of G
the multF of G . ((1_ G),B) is Element of the carrier of G
[(1_ G),B] is set
{(1_ G),B} is non empty set
{{(1_ G),B},{(1_ G)}} is non empty set
the multF of G . [(1_ G),B] is set
(G,e) is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
dom (G,e) is Element of bool the carrier of G
bool the carrier of G is non empty set
C is set
B is set
(G,e) . C is set
(G,e) . B is set
W is Element of the carrier of G
(G,e) . W is Element of the carrier of G
W * e is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (W,e) is Element of the carrier of G
[W,e] is set
{W,e} is non empty set
{W} is non empty trivial 1 -element set
{{W,e},{W}} is non empty set
the multF of G . [W,e] is set
p is Element of the carrier of G
(G,e) . p is Element of the carrier of G
p * e is Element of the carrier of G
the multF of G . (p,e) is Element of the carrier of G
[p,e] is set
{p,e} is non empty set
{p} is non empty trivial 1 -element set
{{p,e},{p}} is non empty set
the multF of G . [p,e] is set
1_ G is non being_of_order_0 Element of the carrier of G
W * (1_ G) is Element of the carrier of G
the multF of G . (W,(1_ G)) is Element of the carrier of G
[W,(1_ G)] is set
{W,(1_ G)} is non empty set
{{W,(1_ G)},{W}} is non empty set
the multF of G . [W,(1_ G)] is set
e " is Element of the carrier of G
e * (e ") is Element of the carrier of G
the multF of G . (e,(e ")) is Element of the carrier of G
[e,(e ")] is set
{e,(e ")} is non empty set
{e} is non empty trivial 1 -element set
{{e,(e ")},{e}} is non empty set
the multF of G . [e,(e ")] is set
W * (e * (e ")) is Element of the carrier of G
the multF of G . (W,(e * (e "))) is Element of the carrier of G
[W,(e * (e "))] is set
{W,(e * (e "))} is non empty set
{{W,(e * (e "))},{W}} is non empty set
the multF of G . [W,(e * (e "))] is set
(W * e) * (e ") is Element of the carrier of G
the multF of G . ((W * e),(e ")) is Element of the carrier of G
[(W * e),(e ")] is set
{(W * e),(e ")} is non empty set
{(W * e)} is non empty trivial 1 -element set
{{(W * e),(e ")},{(W * e)}} is non empty set
the multF of G . [(W * e),(e ")] is set
p * (e * (e ")) is Element of the carrier of G
the multF of G . (p,(e * (e "))) is Element of the carrier of G
[p,(e * (e "))] is set
{p,(e * (e "))} is non empty set
{{p,(e * (e "))},{p}} is non empty set
the multF of G . [p,(e * (e "))] is set
p * (1_ G) is Element of the carrier of G
the multF of G . (p,(1_ G)) is Element of the carrier of G
[p,(1_ G)] is set
{p,(1_ G)} is non empty set
{{p,(1_ G)},{p}} is non empty set
the multF of G . [p,(1_ G)] is set
rng (G,e) is Element of bool the carrier of G
C is set
B is Element of the carrier of G
B * (e ") is Element of the carrier of G
the multF of G . (B,(e ")) is Element of the carrier of G
[B,(e ")] is set
{B,(e ")} is non empty set
{B} is non empty trivial 1 -element set
{{B,(e ")},{B}} is non empty set
the multF of G . [B,(e ")] is set
(G,e) . (B * (e ")) is Element of the carrier of G
(B * (e ")) * e is Element of the carrier of G
the multF of G . ((B * (e ")),e) is Element of the carrier of G
[(B * (e ")),e] is set
{(B * (e ")),e} is non empty set
{(B * (e "))} is non empty trivial 1 -element set
{{(B * (e ")),e},{(B * (e "))}} is non empty set
the multF of G . [(B * (e ")),e] is set
(e ") * e is Element of the carrier of G
the multF of G . ((e "),e) is Element of the carrier of G
[(e "),e] is set
{(e "),e} is non empty set
{(e ")} is non empty trivial 1 -element set
{{(e "),e},{(e ")}} is non empty set
the multF of G . [(e "),e] is set
B * ((e ") * e) is Element of the carrier of G
the multF of G . (B,((e ") * e)) is Element of the carrier of G
[B,((e ") * e)] is set
{B,((e ") * e)} is non empty set
{{B,((e ") * e)},{B}} is non empty set
the multF of G . [B,((e ") * e)] is set
B * (1_ G) is Element of the carrier of G
the multF of G . (B,(1_ G)) is Element of the carrier of G
[B,(1_ G)] is set
{B,(1_ G)} is non empty set
{{B,(1_ G)},{B}} is non empty set
the multF of G . [B,(1_ G)] is set
G is non empty multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
e is Element of bool the carrier of G
A is Element of the carrier of G
(G,A) is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
(G,A) .: e is Element of bool the carrier of G
A * e is Element of bool the carrier of G
{A} is non empty trivial 1 -element Element of bool the carrier of G
{A} * e is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {A} & b2 in e ) } is set
B is set
dom (G,A) is Element of bool the carrier of G
W is set
(G,A) . W is set
p is Element of the carrier of G
(G,A) . p is Element of the carrier of G
A * p is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (A,p) is Element of the carrier of G
[A,p] is set
{A,p} is non empty set
{A} is non empty trivial 1 -element set
{{A,p},{A}} is non empty set
the multF of G . [A,p] is set
B is set
W is Element of the carrier of G
A * W is Element of the carrier of G
the multF of G . (A,W) is Element of the carrier of G
[A,W] is set
{A,W} is non empty set
{{A,W},{A}} is non empty set
the multF of G . [A,W] is set
(G,A) . W is Element of the carrier of G
G is non empty multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
e is Element of bool the carrier of G
A is Element of the carrier of G
(G,A) is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
(G,A) .: e is Element of bool the carrier of G
e * A is Element of bool the carrier of G
{A} is non empty trivial 1 -element Element of bool the carrier of G
e * {A} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in e & b2 in {A} ) } is set
B is set
dom (G,A) is Element of bool the carrier of G
W is set
(G,A) . W is set
p is Element of the carrier of G
(G,A) . p is Element of the carrier of G
p * A is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (p,A) is Element of the carrier of G
[p,A] is set
{p,A} is non empty set
{p} is non empty trivial 1 -element set
{{p,A},{p}} is non empty set
the multF of G . [p,A] is set
B is set
W is Element of the carrier of G
W * A is Element of the carrier of G
the multF of G . (W,A) is Element of the carrier of G
[W,A] is set
{W,A} is non empty set
{W} is non empty trivial 1 -element set
{{W,A},{W}} is non empty set
the multF of G . [W,A] is set
(G,A) . W is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
e is Element of the carrier of G
(G,e) is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total onto bijective Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
(G,e) /" is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
e " is Element of the carrier of G
(G,(e ")) is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total onto bijective Element of bool [: the carrier of G, the carrier of G:]
W is set
rng (G,e) is Element of bool the carrier of G
bool the carrier of G is non empty set
p is Element of the carrier of G
dom (G,e) is Element of bool the carrier of G
(G,(e ")) . p is Element of the carrier of G
((G,e) /") . p is Element of the carrier of G
(G,(e ")) . W is set
(G,e) . ((G,(e ")) . W) is set
e * ((G,(e ")) . p) is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (e,((G,(e ")) . p)) is Element of the carrier of G
[e,((G,(e ")) . p)] is set
{e,((G,(e ")) . p)} is non empty set
{e} is non empty trivial 1 -element set
{{e,((G,(e ")) . p)},{e}} is non empty set
the multF of G . [e,((G,(e ")) . p)] is set
(e ") * p is Element of the carrier of G
the multF of G . ((e "),p) is Element of the carrier of G
[(e "),p] is set
{(e "),p} is non empty set
{(e ")} is non empty trivial 1 -element set
{{(e "),p},{(e ")}} is non empty set
the multF of G . [(e "),p] is set
e * ((e ") * p) is Element of the carrier of G
the multF of G . (e,((e ") * p)) is Element of the carrier of G
[e,((e ") * p)] is set
{e,((e ") * p)} is non empty set
{{e,((e ") * p)},{e}} is non empty set
the multF of G . [e,((e ") * p)] is set
e * (e ") is Element of the carrier of G
the multF of G . (e,(e ")) is Element of the carrier of G
[e,(e ")] is set
{e,(e ")} is non empty set
{{e,(e ")},{e}} is non empty set
the multF of G . [e,(e ")] is set
(e * (e ")) * p is Element of the carrier of G
the multF of G . ((e * (e ")),p) is Element of the carrier of G
[(e * (e ")),p] is set
{(e * (e ")),p} is non empty set
{(e * (e "))} is non empty trivial 1 -element set
{{(e * (e ")),p},{(e * (e "))}} is non empty set
the multF of G . [(e * (e ")),p] is set
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * p is Element of the carrier of G
the multF of G . ((1_ G),p) is Element of the carrier of G
[(1_ G),p] is set
{(1_ G),p} is non empty set
{(1_ G)} is non empty trivial 1 -element set
{{(1_ G),p},{(1_ G)}} is non empty set
the multF of G . [(1_ G),p] is set
B is Relation-like Function-like set
B " is Relation-like Function-like set
(B ") . W is set
B . ((B ") . W) is set
((G,e) /") . W is set
(G,e) . (((G,e) /") . W) is set
dom ((G,e) /") is Element of bool the carrier of G
dom (G,(e ")) is Element of bool the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
e is Element of the carrier of G
(G,e) is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total onto bijective Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
(G,e) /" is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
e " is Element of the carrier of G
(G,(e ")) is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total onto bijective Element of bool [: the carrier of G, the carrier of G:]
W is set
rng (G,e) is Element of bool the carrier of G
bool the carrier of G is non empty set
p is Element of the carrier of G
dom (G,e) is Element of bool the carrier of G
(G,(e ")) . p is Element of the carrier of G
((G,e) /") . p is Element of the carrier of G
(G,(e ")) . W is set
(G,e) . ((G,(e ")) . W) is set
((G,(e ")) . p) * e is Element of the carrier of G
the multF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G . (((G,(e ")) . p),e) is Element of the carrier of G
[((G,(e ")) . p),e] is set
{((G,(e ")) . p),e} is non empty set
{((G,(e ")) . p)} is non empty trivial 1 -element set
{{((G,(e ")) . p),e},{((G,(e ")) . p)}} is non empty set
the multF of G . [((G,(e ")) . p),e] is set
p * (e ") is Element of the carrier of G
the multF of G . (p,(e ")) is Element of the carrier of G
[p,(e ")] is set
{p,(e ")} is non empty set
{p} is non empty trivial 1 -element set
{{p,(e ")},{p}} is non empty set
the multF of G . [p,(e ")] is set
(p * (e ")) * e is Element of the carrier of G
the multF of G . ((p * (e ")),e) is Element of the carrier of G
[(p * (e ")),e] is set
{(p * (e ")),e} is non empty set
{(p * (e "))} is non empty trivial 1 -element set
{{(p * (e ")),e},{(p * (e "))}} is non empty set
the multF of G . [(p * (e ")),e] is set
(e ") * e is Element of the carrier of G
the multF of G . ((e "),e) is Element of the carrier of G
[(e "),e] is set
{(e "),e} is non empty set
{(e ")} is non empty trivial 1 -element set
{{(e "),e},{(e ")}} is non empty set
the multF of G . [(e "),e] is set
p * ((e ") * e) is Element of the carrier of G
the multF of G . (p,((e ") * e)) is Element of the carrier of G
[p,((e ") * e)] is set
{p,((e ") * e)} is non empty set
{{p,((e ") * e)},{p}} is non empty set
the multF of G . [p,((e ") * e)] is set
1_ G is non being_of_order_0 Element of the carrier of G
p * (1_ G) is Element of the carrier of G
the multF of G . (p,(1_ G)) is Element of the carrier of G
[p,(1_ G)] is set
{p,(1_ G)} is non empty set
{{p,(1_ G)},{p}} is non empty set
the multF of G . [p,(1_ G)] is set
B is Relation-like Function-like set
B " is Relation-like Function-like set
(B ") . W is set
B . ((B ") . W) is set
((G,e) /") . W is set
(G,e) . (((G,e) /") . W) is set
dom ((G,e) /") is Element of bool the carrier of G
dom (G,(e ")) is Element of bool the carrier of G
G is TopStruct
the carrier of G is set
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total continuous open Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(id G) /" is Relation-like the carrier of G -defined the carrier of G -defined the carrier of G -valued the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total quasi_total Element of bool [: the carrier of G, the carrier of G:]
G is TopStruct
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total continuous open Element of bool [: the carrier of G, the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
dom (id G) is Element of bool the carrier of G
bool the carrier of G is non empty set
[#] G is non proper dense Element of bool the carrier of G
rng (id G) is Element of bool the carrier of G
(id G) /" is Relation-like the carrier of G -defined the carrier of G -defined the carrier of G -valued the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total quasi_total continuous Element of bool [: the carrier of G, the carrier of G:]
G is non empty TopSpace-like TopStruct
the carrier of G is non empty set
e is Element of the carrier of G
A is a_neighborhood of e
Int A is open Element of bool the carrier of G
bool the carrier of G is non empty set
A ` is Element of bool the carrier of G
the carrier of G \ A is set
Cl (A `) is closed Element of bool the carrier of G
(Cl (A `)) ` is open Element of bool the carrier of G
the carrier of G \ (Cl (A `)) is set
G is non empty TopSpace-like TopStruct
the carrier of G is non empty set
[#] G is non empty non proper open closed dense non boundary Element of bool the carrier of G
bool the carrier of G is non empty set
e is Element of the carrier of G
Int ([#] G) is open Element of bool the carrier of G
([#] G) ` is open closed Element of bool the carrier of G
the carrier of G \ ([#] G) is set
Cl (([#] G) `) is closed Element of bool the carrier of G
(Cl (([#] G) `)) ` is open Element of bool the carrier of G
the carrier of G \ (Cl (([#] G) `)) is set
G is non empty TopSpace-like TopStruct
the carrier of G is non empty set
e is Element of the carrier of G
[#] G is non empty non proper open closed dense non boundary Element of bool the carrier of G
bool the carrier of G is non empty set
A is non empty a_neighborhood of e
G is non empty TopSpace-like TopStruct
the carrier of G is non empty set
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
[: the carrier of G, the carrier of e:] is non empty set
bool [: the carrier of G, the carrier of e:] is non empty set
A is non empty Relation-like the carrier of G -defined the carrier of e -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of e:]
bool the carrier of G is non empty set
C is Element of the carrier of G
A . C is Element of the carrier of e
B is non empty a_neighborhood of C
A .: B is Element of bool the carrier of e
bool the carrier of e is non empty set
Int B is open Element of bool the carrier of G
B ` is Element of bool the carrier of G
the carrier of G \ B is set
Cl (B `) is closed Element of bool the carrier of G
(Cl (B `)) ` is open Element of bool the carrier of G
the carrier of G \ (Cl (B `)) is set
A .: (Int B) is Element of bool the carrier of e
W is non empty open a_neighborhood of A . C
G is non empty TopSpace-like TopStruct
the carrier of G is non empty set
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
[: the carrier of G, the carrier of e:] is non empty set
bool [: the carrier of G, the carrier of e:] is non empty set
A is non empty Relation-like the carrier of G -defined the carrier of e -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of e:]
bool the carrier of G is non empty set
C is Element of bool the carrier of G
A .: C is Element of bool the carrier of e
bool the carrier of e is non empty set
B is set
dom A is Element of bool the carrier of G
W is set
A . W is set
r is Element of bool the carrier of G
p is Element of the carrier of G
A . p is Element of the carrier of e
A .: r is Element of bool the carrier of e
a is non empty a_neighborhood of A . p
Int a is open Element of bool the carrier of e
a ` is Element of bool the carrier of e
the carrier of e \ a is set
Cl (a `) is closed Element of bool the carrier of e
(Cl (a `)) ` is open Element of bool the carrier of e
the carrier of e \ (Cl (a `)) is set
a is open Element of bool the carrier of e
W is Element of bool the carrier of e
G is non empty TopStruct
the carrier of G is non empty set
e is non empty TopStruct
the carrier of e is non empty set
[: the carrier of G, the carrier of e:] is non empty set
bool [: the carrier of G, the carrier of e:] is non empty set
[#] G is non empty non proper dense Element of bool the carrier of G
bool the carrier of G is non empty set
[#] e is non empty non proper dense Element of bool the carrier of e
bool the carrier of e is non empty set
A is non empty Relation-like the carrier of G -defined the carrier of e -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of e:]
dom A is Element of bool the carrier of G
rng A is Element of bool the carrier of e
C is Element of bool the carrier of e
A " C is Element of bool the carrier of G
A .: (A " C) is Element of bool the carrier of e
A /" is non empty Relation-like the carrier of e -defined the carrier of G -valued Function-like V14( the carrier of e) quasi_total Element of bool [: the carrier of e, the carrier of G:]
[: the carrier of e, the carrier of G:] is non empty set
bool [: the carrier of e, the carrier of G:] is non empty set
C is Element of bool the carrier of e
A " C is Element of bool the carrier of G
C is Element of bool the carrier of G
(A /") " C is Element of bool the carrier of e
B is Element of the carrier of G
A . B is Element of the carrier of e
W is Element of the carrier of G
A . W is Element of the carrier of e
A .: C is Element of bool the carrier of e
A " (A .: C) is Element of bool the carrier of G
G is non empty TopStruct
the carrier of G is non empty set
e is non empty TopStruct
the carrier of e is non empty set
[: the carrier of G, the carrier of e:] is non empty set
bool [: the carrier of G, the carrier of e:] is non empty set
[#] G is non empty non proper dense Element of bool the carrier of G
bool the carrier of G is non empty set
[#] e is non empty non proper dense Element of bool the carrier of e
bool the carrier of e is non empty set
A is non empty Relation-like the carrier of G -defined the carrier of e -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of e:]
dom A is Element of bool the carrier of G
rng A is Element of bool the carrier of e
C is Element of bool the carrier of G
A .: C is Element of bool the carrier of e
A " (A .: C) is Element of bool the carrier of G
A /" is non empty Relation-like the carrier of e -defined the carrier of G -valued Function-like V14( the carrier of e) quasi_total Element of bool [: the carrier of e, the carrier of G:]
[: the carrier of e, the carrier of G:] is non empty set
bool [: the carrier of e, the carrier of G:] is non empty set
(A /") " C is Element of bool the carrier of e
A " is Relation-like Function-like set
(A ") " C is set
C is Element of bool the carrier of e
A " C is Element of bool the carrier of G
A .: (A " C) is Element of bool the carrier of e
C is Element of bool the carrier of G
(A /") " C is Element of bool the carrier of e
(A ") " C is set
A .: C is Element of bool the carrier of e
G is non empty TopStruct
the carrier of G is non empty set
e is non empty TopStruct
the carrier of e is non empty set
[: the carrier of G, the carrier of e:] is non empty set
bool [: the carrier of G, the carrier of e:] is non empty set
[#] G is non empty non proper dense Element of bool the carrier of G
bool the carrier of G is non empty set
[#] e is non empty non proper dense Element of bool the carrier of e
bool the carrier of e is non empty set
A is non empty Relation-like the carrier of G -defined the carrier of e -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of e:]
dom A is Element of bool the carrier of G
rng A is Element of bool the carrier of e
C is Element of bool the carrier of e
A " C is Element of bool the carrier of G
A .: (A " C) is Element of bool the carrier of e
C is Element of bool the carrier of G
B is Element of the carrier of G
A . B is Element of the carrier of e
W is Element of the carrier of G
A . W is Element of the carrier of e
A .: C is Element of bool the carrier of e
A " (A .: C) is Element of bool the carrier of G
A /" is non empty Relation-like the carrier of e -defined the carrier of G -valued Function-like V14( the carrier of e) quasi_total Element of bool [: the carrier of e, the carrier of G:]
[: the carrier of e, the carrier of G:] is non empty set
bool [: the carrier of e, the carrier of G:] is non empty set
(A /") " C is Element of bool the carrier of e
G is TopSpace-like TopStruct
the carrier of G is set
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
[: the carrier of G, the carrier of e:] is set
bool [: the carrier of G, the carrier of e:] is non empty set
bool the carrier of e is non empty set
A is Relation-like the carrier of G -defined the carrier of e -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of e:]
[#] e is non empty non proper open closed dense non boundary Element of bool the carrier of e
C is Element of bool the carrier of e
Int C is open Element of bool the carrier of e
C ` is Element of bool the carrier of e
the carrier of e \ C is set
Cl (C `) is closed Element of bool the carrier of e
(Cl (C `)) ` is open Element of bool the carrier of e
the carrier of e \ (Cl (C `)) is set
A " (Int C) is Element of bool the carrier of G
bool the carrier of G is non empty set
A " C is Element of bool the carrier of G
Int (A " (Int C)) is open Element of bool the carrier of G
(A " (Int C)) ` is Element of bool the carrier of G
the carrier of G \ (A " (Int C)) is set
Cl ((A " (Int C)) `) is closed Element of bool the carrier of G
(Cl ((A " (Int C)) `)) ` is open Element of bool the carrier of G
the carrier of G \ (Cl ((A " (Int C)) `)) is set
Int (A " C) is open Element of bool the carrier of G
(A " C) ` is Element of bool the carrier of G
the carrier of G \ (A " C) is set
Cl ((A " C) `) is closed Element of bool the carrier of G
(Cl ((A " C) `)) ` is open Element of bool the carrier of G
the carrier of G \ (Cl ((A " C) `)) is set
C is Element of bool the carrier of e
Int C is open Element of bool the carrier of e
C ` is Element of bool the carrier of e
the carrier of e \ C is set
Cl (C `) is closed Element of bool the carrier of e
(Cl (C `)) ` is open Element of bool the carrier of e
the carrier of e \ (Cl (C `)) is set
A " C is Element of bool the carrier of G
Int (A " C) is open Element of bool the carrier of G
(A " C) ` is Element of bool the carrier of G
the carrier of G \ (A " C) is set
Cl ((A " C) `) is closed Element of bool the carrier of G
(Cl ((A " C) `)) ` is open Element of bool the carrier of G
the carrier of G \ (Cl ((A " C) `)) is set
G is non empty TopSpace-like TopStruct
the carrier of G is non empty set
bool the carrier of G is non empty set
[#] G is non empty non proper open closed dense non boundary Element of bool the carrier of G
G is non empty TopSpace-like TopStruct
the carrier of G is non empty set
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
[: the carrier of G, the carrier of e:] is non empty set
bool [: the carrier of G, the carrier of e:] is non empty set
bool the carrier of G is non empty set
A is non empty Relation-like the carrier of G -defined the carrier of e -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of e:]
C is dense Element of bool the carrier of G
A .: C is Element of bool the carrier of e
bool the carrier of e is non empty set
rng A is Element of bool the carrier of e
[#] e is non empty non proper open closed dense non boundary Element of bool the carrier of e
Cl C is closed Element of bool the carrier of G
[#] G is non empty non proper open closed dense non boundary Element of bool the carrier of G
Cl (A .: C) is closed Element of bool the carrier of e
A .: the carrier of G is Element of bool the carrier of e
G is non empty TopSpace-like TopStruct
the carrier of G is non empty set
e is non empty TopSpace-like TopStruct
the carrier of e is non empty set
[: the carrier of G, the carrier of e:] is non empty set
bool [: the carrier of G, the carrier of e:] is non empty set
bool the carrier of e is non empty set
A is non empty Relation-like the carrier of G -defined the carrier of e -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of e:]
C is dense Element of bool the carrier of e
A " C is Element of bool the carrier of G
bool the carrier of G is non empty set
Cl C is closed Element of bool the carrier of e
[#] e is non empty non proper open closed dense non boundary Element of bool the carrier of e
Cl (A " C) is closed Element of bool the carrier of G
A " (Cl C) is Element of bool the carrier of G
[#] G is non empty non proper open closed dense non boundary Element of bool the carrier of G
G is TopStruct
the carrier of G is set
e is TopStruct
the carrier of e is set
[: the carrier of G, the carrier of e:] is set
bool [: the carrier of G, the carrier of e:] is non empty set
A is Relation-like the carrier of G -defined the carrier of e -valued Function-like quasi_total Element of bool [: the carrier of G, the carrier of e:]
rng A is Element of bool the carrier of e
bool the carrier of e is non empty set
[#] e is non proper dense Element of bool the carrier of e
G is non empty TopStruct
the carrier of G is non empty set
e is non empty TopStruct
the carrier of e is non empty set
[: the carrier of G, the carrier of e:] is non empty set
bool [: the carrier of G, the carrier of e:] is non empty set
A is non empty Relation-like the carrier of G -defined the carrier of e -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of e:]
bool the carrier of G is non empty set
C is Element of bool the carrier of G
A .: C is Element of bool the carrier of e
bool the carrier of e is non empty set
G is TopStruct
the carrier of G is set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total continuous open Element of bool [: the carrier of G, the carrier of G:]
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
G is TopStruct
the carrier of G is set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
e is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total onto bijective continuous being_homeomorphism Element of bool [: the carrier of G, the carrier of G:]
e /" is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
e " is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total onto bijective Element of bool [: the carrier of G, the carrier of G:]
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total continuous open Element of bool [: the carrier of G, the carrier of G:]
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
G is TopStruct
e is TopStruct
the carrier of G is set
the carrier of e is set
[: the carrier of G, the carrier of e:] is set
bool [: the carrier of G, the carrier of e:] is non empty set
G is TopStruct
the carrier of G is set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total continuous open Element of bool [: the carrier of G, the carrier of G:]
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
e is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total (G,G)
G is TopStruct
the carrier of G is set
e is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total (G)
G is TopStruct
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total continuous open Element of bool [: the carrier of G, the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
G is TopStruct
id G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total continuous open Element of bool [: the carrier of G, the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(G) is Relation-like the