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 carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total continuous open (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
the carrier of G is 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 (G)
e /" 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 onto bijective continuous being_homeomorphism 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
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 V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(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 onto bijective continuous being_homeomorphism open (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
A 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 (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 continuous being_homeomorphism (G)
e * A 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:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
G is TopStruct
the carrier of G is set
Funcs ( the carrier of G, the carrier of G) is non empty functional set
e is set
A 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 (G)
A is non empty set
C is Element of A
B is Element of A
W 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 (G)
p 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 (G)
p * W 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:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
r is Element of A
[:A,A:] is non empty set
[:[:A,A:],A:] is non empty set
bool [:[:A,A:],A:] is non empty set
C is non empty Relation-like [:A,A:] -defined A -valued Function-like V14([:A,A:]) quasi_total Element of bool [:[:A,A:],A:]
multMagma(# A,C #) is non empty strict multMagma
B is non empty strict multMagma
the carrier of B is non empty set
the multF of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is non empty set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty set
W is set
p 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 (G)
r 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 (G)
the multF of B . (p,r) is set
[p,r] is set
{p,r} is non empty functional set
{p} is non empty trivial functional 1 -element set
{{p,r},{p}} is non empty set
the multF of B . [p,r] is set
r * p 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:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
a is Element of A
a is Element of A
C . (a,a) is Element of A
[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
C . [a,a] is set
b 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 (G)
m 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 (G)
m * b 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:]
e is strict multMagma
the carrier of e is set
the multF of e is Relation-like [: the carrier of e, the carrier of e:] -defined the carrier of e -valued Function-like quasi_total Element of bool [:[: the carrier of e, the carrier of e:], the carrier of e:]
[: the carrier of e, the carrier of e:] is set
[:[: the carrier of e, the carrier of e:], the carrier of e:] is set
bool [:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty set
A is strict multMagma
the carrier of A is set
the multF of A is Relation-like [: the carrier of A, the carrier of A:] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
[: the carrier of A, the carrier of A:] is set
[:[: the carrier of A, the carrier of A:], the carrier of A:] is set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
C is set
B is set
C is set
B is set
the multF of e . (C,B) is set
[C,B] is set
{C,B} is non empty set
{C} is non empty trivial 1 -element set
{{C,B},{C}} is non empty set
the multF of e . [C,B] is set
the multF of A . (C,B) is set
the multF of A . [C,B] is set
W 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 (G)
p 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 (G)
p * W 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:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
C is set
B is set
G is TopStruct
(G) is strict multMagma
(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 onto bijective continuous being_homeomorphism open (G)
the carrier of G is 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:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
the carrier of (G) is set
G is TopStruct
the carrier of G is set
(G) is non empty strict multMagma
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 (G)
C is Element of the carrier of (G)
A 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 (G)
B is Element of the carrier of (G)
C * 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):] 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,B) is Element of the carrier of (G)
[C,B] is set
{C,B} is non empty set
{C} is non empty trivial 1 -element set
{{C,B},{C}} is non empty set
the multF of (G) . [C,B] is set
A * 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:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
G is TopStruct
(G) is non empty strict multMagma
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) is non empty set
[: 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
(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 onto bijective continuous being_homeomorphism open (G)
the carrier of G is 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:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
C is Element of the carrier of (G)
B is Element of the carrier of (G)
B * C is Element of the carrier of (G)
the multF of (G) . (B,C) is Element of the carrier of (G)
[B,C] is set
{B,C} is non empty set
{B} is non empty trivial 1 -element set
{{B,C},{B}} is non empty set
the multF of (G) . [B,C] is set
C * B is Element of the carrier of (G)
the multF of (G) . (C,B) is Element of the carrier of (G)
[C,B] is set
{C,B} is non empty set
{C} is non empty trivial 1 -element set
{{C,B},{C}} is non empty set
the multF of (G) . [C,B] is set
W 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 (G)
p 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 (G)
p * W 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:]
W * p 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:]
r 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 (G)
dom r 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
r /" 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 onto bijective continuous being_homeomorphism Element of bool [: the carrier of G, the carrier of G:]
a is Element of the carrier of (G)
B * a is Element of the carrier of (G)
the multF of (G) . (B,a) is Element of the carrier of (G)
[B,a] is set
{B,a} is non empty set
{{B,a},{B}} is non empty set
the multF of (G) . [B,a] is set
a * B is Element of the carrier of (G)
the multF of (G) . (a,B) is Element of the carrier of (G)
[a,B] is set
{a,B} is non empty set
{a} is non empty trivial 1 -element set
{{a,B},{a}} is non empty set
the multF of (G) . [a,B] is set
rng r is Element of bool the carrier of G
a 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 (G)
a * r 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:]
r * a 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:]
C is Element of the carrier of (G)
B is Element of the carrier of (G)
C * B is Element of the carrier of (G)
the multF of (G) . (C,B) is Element of the carrier of (G)
[C,B] is set
{C,B} is non empty set
{C} is non empty trivial 1 -element set
{{C,B},{C}} is non empty set
the multF of (G) . [C,B] is set
W is Element of the carrier of (G)
(C * B) * W is Element of the carrier of (G)
the multF of (G) . ((C * B),W) is Element of the carrier of (G)
[(C * B),W] is set
{(C * B),W} is non empty set
{(C * B)} is non empty trivial 1 -element set
{{(C * B),W},{(C * B)}} is non empty set
the multF of (G) . [(C * B),W] is set
B * W is Element of the carrier of (G)
the multF of (G) . (B,W) is Element of the carrier of (G)
[B,W] is set
{B,W} is non empty set
{B} is non empty trivial 1 -element set
{{B,W},{B}} is non empty set
the multF of (G) . [B,W] is set
C * (B * W) is Element of the carrier of (G)
the multF of (G) . (C,(B * W)) is Element of the carrier of (G)
[C,(B * W)] is set
{C,(B * W)} is non empty set
{{C,(B * W)},{C}} is non empty set
the multF of (G) . [C,(B * W)] is set
the carrier of G is set
p 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 (G)
r 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 (G)
r * p 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:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
a 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 (G)
a * r 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:]
the multF of (G) . ((r * p),W) is set
[(r * p),W] is set
{(r * p),W} is non empty set
{(r * p)} is non empty trivial functional 1 -element set
{{(r * p),W},{(r * p)}} is non empty set
the multF of (G) . [(r * p),W] is set
a 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 (G)
a * a 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:]
(a * r) * p 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:]
b 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 (G)
the multF of (G) . (p,b) is set
[p,b] is set
{p,b} is non empty functional set
{p} is non empty trivial functional 1 -element set
{{p,b},{p}} is non empty set
the multF of (G) . [p,b] is set
G is TopStruct
(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 onto bijective continuous being_homeomorphism open (G)
the carrier of G is 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:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is non empty set
(G) is non empty strict unital Group-like associative multMagma
1_ (G) is non being_of_order_0 Element of the carrier of (G)
the carrier of (G) is non empty set
C is Element of the carrier of (G)
A is Element of the carrier of (G)
C * 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 associative 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,A) is Element of the carrier of (G)
[C,A] is set
{C,A} is non empty set
{C} is non empty trivial 1 -element set
{{C,A},{C}} is non empty set
the multF of (G) . [C,A] is set
B 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 (G)
(G) * B 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:]
A * C is Element of the carrier of (G)
the multF of (G) . (A,C) is Element of the carrier of (G)
[A,C] is set
{A,C} is non empty set
{A} is non empty trivial 1 -element set
{{A,C},{A}} is non empty set
the multF of (G) . [A,C] is set
B * (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 onto bijective Element of bool [: the carrier of G, the carrier of G:]
G is TopStruct
the carrier of G is set
(G) is non empty strict unital Group-like associative multMagma
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 (G)
e /" 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 onto bijective continuous being_homeomorphism 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
dom e 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 e is Element of bool the carrier of G
B is Element of the carrier of (G)
B " is Element of the carrier of (G)
C is Element of the carrier of (G)
C * 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 associative 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,B) is Element of the carrier of (G)
[C,B] is set
{C,B} is non empty set
{C} is non empty trivial 1 -element set
{{C,B},{C}} is non empty set
the multF of (G) . [C,B] is set
e * (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:]
(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 onto bijective continuous being_homeomorphism open (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:]
1_ (G) is non being_of_order_0 Element of the carrier of (G)
B * C is Element of the carrier of (G)
the multF of (G) . (B,C) is Element of the carrier of (G)
[B,C] is set
{B,C} is non empty set
{B} is non empty trivial 1 -element set
{{B,C},{B}} is non empty set
the multF of (G) . [B,C] is set
(e /") * 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:]
G is non empty trivial V43() 1 -element TopStruct
the carrier of G is non empty trivial V28() 1 -element set
e is Element of the carrier of G
A is Element of the carrier of G
(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 continuous being_homeomorphism open (G)
id the carrier of 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 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 set
(G) . e is Element of 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
{e} is non empty trivial 1 -element compact Element of bool the carrier of G
bool the carrier of G is non empty set
A is Element of the carrier of G
C 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 continuous being_homeomorphism open (G)
C . e is Element of the carrier of G
dom C is Element of bool the carrier of G
Im (C,e) is set
{e} is non empty trivial 1 -element set
C .: {e} is set
{(C . e)} is non empty trivial 1 -element compact Element of bool the carrier of G
{A} is non empty trivial 1 -element compact Element of bool the carrier of G
G is non empty TopSpace-like () TopStruct
the carrier of G is non empty set
bool 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
C is Element of the carrier of G
A is open Element of bool the carrier of G
B 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 continuous being_homeomorphism open (G)
B . e is Element of the carrier of G
B " A is Element of bool the carrier of G
dom B is Element of bool the carrier of G
rng B is Element of bool the carrier of G
W is Relation-like Function-like set
W " is Relation-like Function-like set
(W ") . C is set
B " 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
(B ") . C is Element of the carrier of G
W . ((W ") . C) is set
W " A is set
p is Element of bool the carrier of G
Cl p is closed Element of bool the carrier of G
B .: p is Element of bool the carrier of G
r is open Element of bool the carrier of G
a is open Element of bool the carrier of G
B .: (Cl p) is Element of bool the carrier of G
Cl a is closed Element of bool the carrier of G
B .: (B " A) is Element of bool the carrier of G
G is non empty set
[:G,G:] is non empty set
[:[:G,G:],G:] is non empty set
bool [:[:G,G:],G:] is non empty set
bool G is non empty set
bool (bool G) is non empty set
e is non empty Relation-like [:G,G:] -defined G -valued Function-like V14([:G,G:]) quasi_total Element of bool [:[:G,G:],G:]
A is Element of bool (bool G)
(G,e,A) is () ()
G is set
{G} is non empty trivial 1 -element set
[:{G},{G}:] is non empty set
[:[:{G},{G}:],{G}:] is non empty set
bool [:[:{G},{G}:],{G}:] is non empty set
bool {G} is non empty set
bool (bool {G}) is non empty set
e is non empty Relation-like [:{G},{G}:] -defined {G} -valued Function-like V14([:{G},{G}:]) quasi_total Element of bool [:[:{G},{G}:],{G}:]
A is Element of bool (bool {G})
({G},e,A) is non empty () ()
G is non empty trivial V43() 1 -element multMagma
the carrier of G is non empty trivial V28() 1 -element set
the Element of the carrier of G is Element of the carrier of G
C is Element of the carrier of G
A is Element of the carrier of G
C * 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:] 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,A) is Element of the carrier of G
[C,A] is set
{C,A} is non empty set
{C} is non empty trivial 1 -element set
{{C,A},{C}} is non empty set
the multF of G . [C,A] is set
A * C is Element of the carrier of G
the multF of G . (A,C) is Element of the carrier of G
[A,C] is set
{A,C} is non empty set
{A} is non empty trivial 1 -element set
{{A,C},{A}} is non empty set
the multF of G . [A,C] is set
B is Element of the carrier of G
C * B is Element of the carrier of G
the multF of G . (C,B) is Element of the carrier of G
[C,B] is set
{C,B} is non empty set
{{C,B},{C}} is non empty set
the multF of G . [C,B] is set
B * C is Element of the carrier of G
the multF of G . (B,C) is Element of the carrier of G
[B,C] is set
{B,C} is non empty set
{B} is non empty trivial 1 -element set
{{B,C},{B}} is non empty set
the multF of G . [B,C] is set
e is Element of the carrier of G
A is Element of the carrier of G
e * A is Element of the carrier of G
the multF of G . (e,A) is Element of the carrier of G
[e,A] is set
{e,A} is non empty set
{e} is non empty trivial 1 -element set
{{e,A},{e}} is non empty set
the multF of G . [e,A] is set
C is Element of the carrier of G
(e * A) * C is Element of the carrier of G
the multF of G . ((e * A),C) is Element of the carrier of G
[(e * A),C] is set
{(e * A),C} is non empty set
{(e * A)} is non empty trivial 1 -element set
{{(e * A),C},{(e * A)}} is non empty set
the multF of G . [(e * A),C] is set
A * C is Element of the carrier of G
the multF of G . (A,C) is Element of the carrier of G
[A,C] is set
{A,C} is non empty set
{A} is non empty trivial 1 -element set
{{A,C},{A}} is non empty set
the multF of G . [A,C] is set
e * (A * C) is Element of the carrier of G
the multF of G . (e,(A * C)) is Element of the carrier of G
[e,(A * C)] is set
{e,(A * C)} is non empty set
{{e,(A * C)},{e}} is non empty set
the multF of G . [e,(A * C)] is set
e is Element of the carrier of G
A is Element of the carrier of G
e * A is Element of the carrier of G
the multF of G . (e,A) is Element of the carrier of G
[e,A] is set
{e,A} is non empty set
{e} is non empty trivial 1 -element set
{{e,A},{e}} is non empty set
the multF of G . [e,A] is set
A * e is Element of the carrier of G
the multF of G . (A,e) is Element of the carrier of G
[A,e] is set
{A,e} is non empty set
{A} is non empty trivial 1 -element set
{{A,e},{A}} is non empty set
the multF of G . [A,e] is set
G is set
{G} is non empty trivial 1 -element set
1TopSp {G} is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
bool {G} is non empty Element of bool (bool {G})
bool {G} is non empty set
bool (bool {G}) is non empty set
[#] (bool {G}) is non empty non proper Element of bool (bool {G})
bool (bool {G}) is non empty set
TopStruct(# {G},([#] (bool {G})) #) is non empty strict TopStruct
{{}} is non empty trivial 1 -element set
[:{{}},{{}}:] is non empty set
[:[:{{}},{{}}:],{{}}:] is non empty set
bool [:[:{{}},{{}}:],{{}}:] is non empty set
the non empty Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V14([:{{}},{{}}:]) quasi_total Element of bool [:[:{{}},{{}}:],{{}}:] is non empty Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V14([:{{}},{{}}:]) quasi_total Element of bool [:[:{{}},{{}}:],{{}}:]
bool {{}} is non empty set
bool (bool {{}}) is non empty set
the Element of bool (bool {{}}) is Element of bool (bool {{}})
({{}}, the non empty Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V14([:{{}},{{}}:]) quasi_total Element of bool [:[:{{}},{{}}:],{{}}:], the Element of bool (bool {{}})) is non empty trivial V43() 1 -element unital Group-like associative commutative () () ()
{{}} is non empty trivial 1 -element set
[:{{}},{{}}:] is non empty set
[:[:{{}},{{}}:],{{}}:] is non empty set
bool [:[:{{}},{{}}:],{{}}:] is non empty set
the non empty Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V14([:{{}},{{}}:]) quasi_total Element of bool [:[:{{}},{{}}:],{{}}:] is non empty Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V14([:{{}},{{}}:]) quasi_total Element of bool [:[:{{}},{{}}:],{{}}:]
bool {{}} is non empty Element of bool (bool {{}})
bool {{}} is non empty set
bool (bool {{}}) is non empty set
({{}}, the non empty Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V14([:{{}},{{}}:]) quasi_total Element of bool [:[:{{}},{{}}:],{{}}:],(bool {{}})) is non empty trivial V43() 1 -element unital Group-like associative commutative () () ()
1TopSp {{}} is non empty trivial V43() 1 -element strict TopSpace-like T_0 T_1 T_2 compact () TopStruct
[#] (bool {{}}) is non empty non proper Element of bool (bool {{}})
bool (bool {{}}) is non empty set
TopStruct(# {{}},([#] (bool {{}})) #) is non empty strict TopStruct
the carrier of (1TopSp {{}}) is non empty trivial V28() 1 -element set
{{}} is non empty trivial 1 -element set
[:{{}},{{}}:] is non empty set
[:[:{{}},{{}}:],{{}}:] is non empty set
bool [:[:{{}},{{}}:],{{}}:] is non empty set
the non empty Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V14([:{{}},{{}}:]) quasi_total Element of bool [:[:{{}},{{}}:],{{}}:] is non empty Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V14([:{{}},{{}}:]) quasi_total Element of bool [:[:{{}},{{}}:],{{}}:]
1TopSp {{}} is non empty trivial V43() 1 -element strict TopSpace-like T_0 T_1 T_2 compact () TopStruct
bool {{}} is non empty Element of bool (bool {{}})
bool {{}} is non empty set
bool (bool {{}}) is non empty set
[#] (bool {{}}) is non empty non proper Element of bool (bool {{}})
bool (bool {{}}) is non empty set
TopStruct(# {{}},([#] (bool {{}})) #) is non empty strict TopStruct
({{}}, the non empty Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V14([:{{}},{{}}:]) quasi_total Element of bool [:[:{{}},{{}}:],{{}}:],(bool {{}})) is non empty trivial V43() 1 -element unital Group-like associative commutative () () ()
e is non empty trivial V43() 1 -element TopSpace-like compact unital Group-like associative commutative () () ()
inverse_op e is non empty Relation-like the carrier of e -defined the carrier of e -valued Function-like one-to-one V14( the carrier of e) quasi_total onto bijective Element of bool [: the carrier of e, the carrier of e:]
the carrier of e is non empty trivial V28() 1 -element set
[: the carrier of e, the carrier of e:] is non empty set
bool [: the carrier of e, the carrier of e:] is non empty set
bool the carrier of e is non empty set
C is trivial Element of bool the carrier of e
(inverse_op e) " C is trivial Element of bool the carrier of e
[#] e is non empty trivial non proper 1 -element open closed dense non boundary Element of bool the carrier of e
[:e,e:] is non empty strict TopSpace-like TopStruct
the carrier of [:e,e:] is non empty set
[: the carrier of [:e,e:], the carrier of e:] is non empty set
bool [: the carrier of [:e,e:], the carrier of e:] is non empty set
A is non empty Relation-like the carrier of [:e,e:] -defined the carrier of e -valued Function-like V14( the carrier of [:e,e:]) quasi_total Element of bool [: the carrier of [:e,e:], the carrier of e:]
the multF of e is non empty Relation-like [: the carrier of e, the carrier of e:] -defined the carrier of e -valued Function-like V14([: the carrier of e, the carrier of e:]) quasi_total associative Element of bool [:[: the carrier of e, the carrier of e:], the carrier of e:]
[:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty set
bool [:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty set
[{},{}] is set
{{},{}} is non empty set
{{{},{}},{{}}} is non empty set
{[{},{}]} is non empty trivial Function-like 1 -element set
bool the carrier of e is non empty set
C is trivial Element of bool the carrier of e
A " C is Element of bool the carrier of [:e,e:]
bool the carrier of [:e,e:] is non empty set
[#] [:e,e:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:e,e:]
G is non empty TopSpace-like () ()
the carrier of G is non empty set
e is Element of the carrier of G
A is Element of the carrier of G
e * 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:] 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 . (e,A) is Element of the carrier of G
[e,A] is set
{e,A} is non empty set
{e} is non empty trivial 1 -element set
{{e,A},{e}} is non empty set
the multF of G . [e,A] is set
C is non empty a_neighborhood of e * A
[:G,G:] is non empty strict TopSpace-like TopStruct
the carrier of [:G,G:] is non empty set
[: the carrier of [:G,G:], the carrier of G:] is non empty set
bool [: the carrier of [:G,G:], the carrier of G:] is non empty set
B is non empty Relation-like the carrier of [:G,G:] -defined the carrier of G -valued Function-like V14( the carrier of [:G,G:]) quasi_total Element of bool [: the carrier of [:G,G:], the carrier of G:]
[e,A] is Element of the carrier of [:G,G:]
W is non empty a_neighborhood of [e,A]
B .: W is Element of bool the carrier of G
bool the carrier of G is non empty set
bool the carrier of [:G,G:] is non empty set
bool (bool the carrier of [:G,G:]) is non empty set
Int W is open Element of bool the carrier of [:G,G:]
W ` is Element of bool the carrier of [:G,G:]
the carrier of [:G,G:] \ W is set
Cl (W `) is closed Element of bool the carrier of [:G,G:]
(Cl (W `)) ` is open Element of bool the carrier of [:G,G:]
the carrier of [:G,G:] \ (Cl (W `)) is set
p is Element of bool (bool the carrier of [:G,G:])
union p is Element of bool the carrier of [:G,G:]
r is set
a is Element of bool the carrier of G
a is Element of bool the carrier of G
[:a,a:] is Element of bool the carrier of [:G,G:]
Int a is open Element of bool the carrier of G
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
Int a is open Element of bool the carrier of G
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
m is non empty open a_neighborhood of e
b is non empty open a_neighborhood of A
m * b is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in m & b2 in b ) } is set
q is set
g is Element of the carrier of G
h is Element of the carrier of G
g * h is Element of the carrier of G
the multF of G . (g,h) is Element of the carrier of G
[g,h] is set
{g,h} is non empty set
{g} is non empty trivial 1 -element set
{{g,h},{g}} is non empty set
the multF of G . [g,h] is set
[g,h] is Element of the carrier of [:G,G:]
G is non empty TopSpace-like ()
the carrier of G is non empty set
[:G,G:] is non empty strict TopSpace-like TopStruct
the carrier of [:G,G:] is non empty set
[: the carrier of [:G,G:], the carrier of G:] is non empty set
bool [: the carrier of [:G,G:], the carrier of G:] is non empty set
e is non empty Relation-like the carrier of [:G,G:] -defined the carrier of G -valued Function-like V14( the carrier of [:G,G:]) quasi_total Element of bool [: the carrier of [:G,G:], 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
A is Element of the carrier of [:G,G:]
e . A is Element of the carrier of G
C is non empty a_neighborhood of e . A
B is Element of the carrier of G
W is Element of the carrier of G
[B,W] is Element of the carrier of [:G,G:]
{B,W} is non empty set
{B} is non empty trivial 1 -element set
{{B,W},{B}} is non empty set
B * W is Element of the carrier of G
the multF of G . (B,W) is Element of the carrier of G
[B,W] is set
the multF of G . [B,W] is set
p is non empty a_neighborhood of B
r is non empty a_neighborhood of W
p * r is Element of bool the carrier of G
bool the carrier of G is non empty set
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in p & b2 in r ) } is set
[:p,r:] is non empty a_neighborhood of [B,W]
a is non empty a_neighborhood of A
e .: a is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () ()
the carrier of G is non empty set
e is Element of the carrier of G
e " is Element of the carrier of G
A is non empty a_neighborhood of e "
[: 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:]
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:]
C . e is Element of the carrier of G
B is non empty a_neighborhood of e
C .: B is Element of bool the carrier of G
bool the carrier of G 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
Int (Int B) is open Element of bool the carrier of G
(Int B) ` is closed Element of bool the carrier of G
the carrier of G \ (Int B) is set
Cl ((Int B) `) is closed Element of bool the carrier of G
(Cl ((Int B) `)) ` is open Element of bool the carrier of G
the carrier of G \ (Cl ((Int B) `)) is set
W is non empty open a_neighborhood of e
W " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in W } is set
p is set
r is Element of the carrier of G
r " is Element of the carrier of G
C . r is Element of the carrier of G
G is non empty TopSpace-like unital Group-like associative ()
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
A is Element of the carrier of G
(inverse_op G) . A is Element of the carrier of G
C is non empty a_neighborhood of (inverse_op G) . A
A " is Element of the carrier of G
B is non empty a_neighborhood of A
B " is Element of bool the carrier of G
bool the carrier of G is non empty set
{ (b1 ") where b1 is Element of the carrier of G : b1 in B } is set
(inverse_op G) .: B is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
e is Element of the carrier of G
A is Element of the carrier of G
A " is Element of the carrier of G
e * (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 associative 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 . (e,(A ")) is Element of the carrier of G
[e,(A ")] is set
{e,(A ")} is non empty set
{e} is non empty trivial 1 -element set
{{e,(A ")},{e}} is non empty set
the multF of G . [e,(A ")] is set
C is non empty a_neighborhood of e * (A ")
B is non empty open a_neighborhood of e
W is non empty open a_neighborhood of A "
B * W is Element of bool the carrier of G
bool the carrier of G is non empty set
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B & b2 in W ) } is set
p is non empty open a_neighborhood of A
p " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in p } is set
B * (p ") is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B & b2 in p " ) } is set
r is 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 Element of the carrier of G
b " is Element of the carrier of G
a * (b ") is Element of the carrier of G
the multF of G . (a,(b ")) is Element of the carrier of G
[a,(b ")] is set
{a,(b ")} is non empty set
{{a,(b ")},{a}} is non empty set
the multF of G . [a,(b ")] is set
G is non empty TopSpace-like unital Group-like associative ()
the carrier of G is non empty set
e is Element of the carrier of G
e " is Element of the carrier of G
A is non empty a_neighborhood of e "
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * (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:] 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 . ((1_ G),(e ")) is Element of the carrier of G
[(1_ G),(e ")] is set
{(1_ G),(e ")} is non empty set
{(1_ G)} is non empty trivial 1 -element set
{{(1_ G),(e ")},{(1_ G)}} is non empty set
the multF of G . [(1_ G),(e ")] is set
C is non empty a_neighborhood of 1_ G
B is non empty a_neighborhood of e
B " is Element of bool the carrier of G
bool the carrier of G is non empty set
{ (b1 ") where b1 is Element of the carrier of G : b1 in B } is set
C * (B ") 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 B " ) } is set
W is set
p is Element of the carrier of G
p " is 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),(p ")},{(1_ G)}} is non empty set
the multF of G . [(1_ G),(p ")] is set
e is Element of the carrier of G
A is Element of the carrier of G
e * 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 associative 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 . (e,A) is Element of the carrier of G
[e,A] is set
{e,A} is non empty set
{e} is non empty trivial 1 -element set
{{e,A},{e}} is non empty set
the multF of G . [e,A] is set
C is non empty a_neighborhood of e * A
A " is Element of the carrier of G
(A ") " is Element of the carrier of G
e * ((A ") ") is Element of the carrier of G
the multF of G . (e,((A ") ")) is Element of the carrier of G
[e,((A ") ")] is set
{e,((A ") ")} is non empty set
{{e,((A ") ")},{e}} is non empty set
the multF of G . [e,((A ") ")] is set
B is non empty a_neighborhood of e
W is non empty a_neighborhood of A "
W " is Element of bool the carrier of G
bool the carrier of G is non empty set
{ (b1 ") where b1 is Element of the carrier of G : b1 in W } is set
B * (W ") is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B & b2 in W " ) } is set
p is non empty a_neighborhood of A
p " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in p } is set
B * p is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B & b2 in p ) } is set
r is 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
a " is Element of the carrier of G
G is non empty TopSpace-like () ()
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
C is Element of the carrier of G
(G,e) . C is Element of the carrier of G
B is non empty a_neighborhood of (G,e) . C
e * 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:], 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,C) is Element of the carrier of G
[e,C] is set
{e,C} is non empty set
{e} is non empty trivial 1 -element set
{{e,C},{e}} is non empty set
the multF of G . [e,C] is set
W is non empty open a_neighborhood of e
p is non empty open a_neighborhood of C
W * p is Element of bool the carrier of G
bool the carrier of G is non empty set
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in W & b2 in p ) } is set
(G,e) .: p is Element of bool the carrier of G
r is set
e * p is Element of bool the carrier of G
{e} is non empty trivial 1 -element compact Element of bool the carrier of G
{e} * p 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 p ) } is set
a is Element of the carrier of G
e * a is Element of the carrier of G
the multF of G . (e,a) is Element of the carrier of G
[e,a] is set
{e,a} is non empty set
{{e,a},{e}} is non empty set
the multF of G . [e,a] 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:]
C is Element of the carrier of G
(G,e) . C is Element of the carrier of G
B is non empty a_neighborhood of (G,e) . C
C * 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 . (C,e) is Element of the carrier of G
[C,e] is set
{C,e} is non empty set
{C} is non empty trivial 1 -element set
{{C,e},{C}} is non empty set
the multF of G . [C,e] is set
W is non empty open a_neighborhood of C
p is non empty open a_neighborhood of e
W * p is Element of bool the carrier of G
bool the carrier of G is non empty set
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in W & b2 in p ) } is set
(G,e) .: W is Element of bool the carrier of G
r is set
W * e is Element of bool the carrier of G
{e} is non empty trivial 1 -element compact Element of bool the carrier of G
W * {e} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in W & b2 in {e} ) } is set
a is Element of the carrier of G
a * e is Element of the carrier of G
the multF of G . (a,e) is Element of the carrier of G
[a,e] is set
{a,e} is non empty set
{a} is non empty trivial 1 -element set
{{a,e},{a}} is non empty set
the multF of G . [a,e] is set
G is non empty TopSpace-like unital Group-like associative () ()
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 continuous 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
[#] G is non empty non proper open closed dense non boundary Element of bool the carrier of G
rng (G,e) is Element of bool 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:]
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 continuous Element of bool [: the carrier of G, the carrier of G:]
G is non empty TopSpace-like unital Group-like associative () ()
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 continuous 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
[#] G is non empty non proper open closed dense non boundary Element of bool the carrier of G
rng (G,e) is Element of bool 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:]
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 continuous Element of bool [: the carrier of G, the carrier of G:]
G is non empty TopSpace-like unital Group-like associative () ()
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 continuous 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 one-to-one V14( the carrier of G) quasi_total onto bijective continuous Element of bool [: the carrier of G, the carrier of G:]
G is non empty TopSpace-like unital Group-like associative () ()
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 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
dom (inverse_op G) is Element of bool the carrier of G
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
rng (inverse_op G) is Element of bool the carrier of G
(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:]
(inverse_op G) " is Relation-like Function-like one-to-one set
G is non empty TopSpace-like unital Group-like associative () ()
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 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
G is non empty TopSpace-like unital Group-like associative ()
e is non empty TopSpace-like unital Group-like associative () ()
the carrier of e is non empty set
A is Element of the carrier of e
C is Element of the carrier of e
A " is Element of the carrier of e
(A ") * C is Element of the carrier of e
the multF of e is non empty Relation-like [: the carrier of e, the carrier of e:] -defined the carrier of e -valued Function-like V14([: the carrier of e, the carrier of e:]) quasi_total associative Element of bool [:[: the carrier of e, the carrier of e:], the carrier of e:]
[: the carrier of e, the carrier of e:] is non empty set
[:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty set
bool [:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty set
the multF of e . ((A "),C) is Element of the carrier of e
[(A "),C] is set
{(A "),C} is non empty set
{(A ")} is non empty trivial 1 -element set
{{(A "),C},{(A ")}} is non empty set
the multF of e . [(A "),C] is set
(e,((A ") * C)) is non empty Relation-like the carrier of e -defined the carrier of e -valued Function-like one-to-one V14( the carrier of e) quasi_total onto bijective continuous being_homeomorphism open (e)
(e,((A ") * C)) . A is set
(e,((A ") * C)) . A is Element of the carrier of e
A * ((A ") * C) is Element of the carrier of e
the multF of e . (A,((A ") * C)) is Element of the carrier of e
[A,((A ") * C)] is set
{A,((A ") * C)} is non empty set
{A} is non empty trivial 1 -element set
{{A,((A ") * C)},{A}} is non empty set
the multF of e . [A,((A ") * C)] is set
A * (A ") is Element of the carrier of e
the multF of e . (A,(A ")) is Element of the carrier of e
[A,(A ")] is set
{A,(A ")} is non empty set
{{A,(A ")},{A}} is non empty set
the multF of e . [A,(A ")] is set
(A * (A ")) * C is Element of the carrier of e
the multF of e . ((A * (A ")),C) is Element of the carrier of e
[(A * (A ")),C] is set
{(A * (A ")),C} is non empty set
{(A * (A "))} is non empty trivial 1 -element set
{{(A * (A ")),C},{(A * (A "))}} is non empty set
the multF of e . [(A * (A ")),C] is set
1_ e is non being_of_order_0 Element of the carrier of e
(1_ e) * C is Element of the carrier of e
the multF of e . ((1_ e),C) is Element of the carrier of e
[(1_ e),C] is set
{(1_ e),C} is non empty set
{(1_ e)} is non empty trivial 1 -element set
{{(1_ e),C},{(1_ e)}} is non empty set
the multF of e . [(1_ e),C] is set
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is closed Element of bool the carrier of G
A is Element of the carrier of G
e * A is Element of bool the carrier of G
{A} is non empty trivial 1 -element compact 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
(G,A) 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 continuous being_homeomorphism open (G)
(G,A) .: e is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is closed Element of bool the carrier of G
A is Element of the carrier of G
A * e is Element of bool the carrier of G
{A} is non empty trivial 1 -element compact 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
(G,A) 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 continuous being_homeomorphism open (G)
(G,A) .: e is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
A is Element of the carrier of G
e is closed Element of bool the carrier of G
e * A is Element of bool the carrier of G
{A} is non empty trivial 1 -element compact 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
A * e is 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
G is non empty TopSpace-like unital Group-like associative () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is closed 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
(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 continuous being_homeomorphism open (G)
(G) .: e is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is closed 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
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is open Element of bool the carrier of G
A is Element of the carrier of G
e * A is Element of bool the carrier of G
{A} is non empty trivial 1 -element compact 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
(G,A) 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 continuous being_homeomorphism open (G)
(G,A) .: e is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is open Element of bool the carrier of G
A is Element of the carrier of G
A * e is Element of bool the carrier of G
{A} is non empty trivial 1 -element compact 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
(G,A) 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 continuous being_homeomorphism open (G)
(G,A) .: e is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
A is Element of the carrier of G
e is open Element of bool the carrier of G
e * A is Element of bool the carrier of G
{A} is non empty trivial 1 -element compact 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
A * e is 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
G is non empty TopSpace-like unital Group-like associative () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is open 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
(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 continuous being_homeomorphism open (G)
(G) .: e is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is open 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
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
A is Element of bool the carrier of G
e is 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
Int (A * e) is open Element of bool the carrier of G
(A * e) ` is Element of bool the carrier of G
the carrier of G \ (A * e) is set
Cl ((A * e) `) is closed Element of bool the carrier of G
(Cl ((A * e) `)) ` is open Element of bool the carrier of G
the carrier of G \ (Cl ((A * e) `)) is set
C is set
B is Element of the carrier of G
W is Element of the carrier of G
B * 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:] 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 . (B,W) is Element of the carrier of G
[B,W] is set
{B,W} is non empty set
{B} is non empty trivial 1 -element set
{{B,W},{B}} is non empty set
the multF of G . [B,W] is set
A * W is Element of bool the carrier of G
{W} is non empty trivial 1 -element compact Element of bool the carrier of G
A * {W} 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 {W} ) } is set
r is set
a 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} is non empty trivial 1 -element set
{{a,W},{a}} is non empty set
the multF of G . [a,W] is set
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
A is Element of bool the carrier of G
e 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
Int (e * A) is open Element of bool the carrier of G
(e * A) ` is Element of bool the carrier of G
the carrier of G \ (e * A) is set
Cl ((e * A) `) is closed Element of bool the carrier of G
(Cl ((e * A) `)) ` is open Element of bool the carrier of G
the carrier of G \ (Cl ((e * A) `)) is set
C is set
B is Element of the carrier of G
W is Element of the carrier of G
B * 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:] 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 . (B,W) is Element of the carrier of G
[B,W] is set
{B,W} is non empty set
{B} is non empty trivial 1 -element set
{{B,W},{B}} is non empty set
the multF of G . [B,W] is set
B * A is Element of bool the carrier of G
{B} is non empty trivial 1 -element compact Element of bool the carrier of G
{B} * A is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {B} & b2 in A ) } is set
r is set
a is Element of the carrier of G
B * a is Element of the carrier of G
the multF of G . (B,a) is Element of the carrier of G
[B,a] is set
{B,a} is non empty set
{{B,a},{B}} is non empty set
the multF of G . [B,a] is set
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is open Element of bool the carrier of G
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
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
G is non empty TopSpace-like unital Group-like associative () ()
the carrier of G is non empty set
e is Element of the carrier of G
e " is Element of the carrier of G
A is non empty a_neighborhood of e
A " is Element of bool the carrier of G
bool the carrier of G is non empty set
{ (b1 ") where b1 is Element of the carrier of G : b1 in A } is set
Int A is open Element of bool the carrier of G
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
C is Element of bool the carrier of G
C " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in C } is set
Int (A ") is open Element of bool the carrier of G
(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 unital Group-like associative () () () ()
the carrier of G is non empty set
e is Element of the carrier of G
e " is Element of the carrier of G
e * (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:] 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 . (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
A is non empty a_neighborhood of e * (e ")
C is non empty open a_neighborhood of e
B is non empty open a_neighborhood of e
B " is open Element of bool the carrier of G
bool the carrier of G is non empty set
{ (b1 ") where b1 is Element of the carrier of G : b1 in B } is set
C * (B ") is open Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in C & b2 in B " ) } is set
C /\ B is open Element of bool the carrier of G
W is non empty open a_neighborhood of e
W " is open Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in W } is set
W * (W ") is open Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in W & b2 in W " ) } is set
p is set
r is Element of the carrier of G
a is Element of the carrier of G
r * a is Element of the carrier of G
the multF of G . (r,a) is Element of the carrier of G
[r,a] is set
{r,a} is non empty set
{r} is non empty trivial 1 -element set
{{r,a},{r}} is non empty set
the multF of G . [r,a] is set
a " is Element of the carrier of G
G is non empty TopSpace-like unital Group-like associative () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is dense 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
(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 continuous being_homeomorphism open (G)
(G) " e is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is dense 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
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is dense Element of bool the carrier of G
A is Element of the carrier of G
A * e is Element of bool the carrier of G
{A} is non empty trivial 1 -element compact 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
(G,A) 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 continuous being_homeomorphism open (G)
(G,A) .: e is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
e is dense Element of bool the carrier of G
A is Element of the carrier of G
e * A is Element of bool the carrier of G
{A} is non empty trivial 1 -element compact 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
(G,A) 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 continuous being_homeomorphism open (G)
(G,A) .: e is Element of bool the carrier of G
G is non empty TopSpace-like unital Group-like associative () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
A is Element of the carrier of G
e is dense Element of bool the carrier of G
e * A is Element of bool the carrier of G
{A} is non empty trivial 1 -element compact 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
A * e is 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
G is non empty TopSpace-like unital Group-like associative () () () ()
1_ G is non being_of_order_0 Element of the carrier of G
the carrier of G is non empty set
bool the carrier of G is non empty set
bool (bool the carrier of G) is non empty set
e is open V182(G, 1_ G) Element of bool (bool the carrier of G)
A is dense Element of bool the carrier of G
{ (b1 * b2) where b1 is Element of bool the carrier of G, b2 is Element of the carrier of G : ( b1 in e & b2 in A ) } is set
the topology of G is non empty open Element of bool (bool the carrier of G)
B is set
p is Element of the carrier of G
W is Element of bool the carrier of G
W * p is Element of bool the carrier of G
{p} is non empty trivial 1 -element compact Element of bool the carrier of G
W * {p} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in W & b2 in {p} ) } is set
r is Element of bool the carrier of G
(1_ G) " is Element of the carrier of G
(1_ G) * ((1_ G) ") 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:] 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 . ((1_ G),((1_ G) ")) is Element of the carrier of G
[(1_ G),((1_ G) ")] is set
{(1_ G),((1_ G) ")} is non empty set
{(1_ G)} is non empty trivial 1 -element set
{{(1_ G),((1_ G) ")},{(1_ G)}} is non empty set
the multF of G . [(1_ G),((1_ G) ")] is set
(1_ G) * (1_ G) is Element of the carrier of G
the multF of G . ((1_ G),(1_ G)) is Element of the carrier of G
[(1_ G),(1_ G)] is set
{(1_ G),(1_ G)} is non empty set
{{(1_ G),(1_ G)},{(1_ G)}} is non empty set
the multF of G . [(1_ G),(1_ G)] is set
B is Element of bool the carrier of G
W is Element of the carrier of G
W " is Element of the carrier of G
W * (W ") is Element of the carrier of G
the multF of G . (W,(W ")) is Element of the carrier of G
[W,(W ")] is set
{W,(W ")} is non empty set
{W} is non empty trivial 1 -element set
{{W,(W ")},{W}} is non empty set
the multF of G . [W,(W ")] is set
B * (W ") is Element of bool the carrier of G
{(W ")} is non empty trivial 1 -element compact Element of bool the carrier of G
B * {(W ")} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B & b2 in {(W ")} ) } is set
p is non empty open a_neighborhood of 1_ G
p " is open Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in p } is set
p * (p ") is open Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in p & b2 in p " ) } is set
r is Element of bool the carrier of G
A " is dense Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in A } is set
W * (A ") is dense Element of bool the carrier of G
{W} is non empty trivial 1 -element compact Element of bool the carrier of G
{W} * (A ") is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {W} & b2 in A " ) } is set
(W * (A ")) /\ r is Element of bool the carrier of G
a is set
a is Element of the carrier of G
a " 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 ")} is non empty trivial 1 -element set
{{(a "),W},{(a ")}} is non empty set
the multF of G . [(a "),W] is set
r * ((a ") * W) is Element of bool the carrier of G
{((a ") * W)} is non empty trivial 1 -element compact Element of bool the carrier of G
r * {((a ") * W)} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in r & b2 in {((a ") * W)} ) } is set
b is Element of bool the carrier of G
m is Element of the carrier of G
W * m is Element of the carrier of G
the multF of G . (W,m) is Element of the carrier of G
[W,m] is set
{W,m} is non empty set
{{W,m},{W}} is non empty set
the multF of G . [W,m] is set
((a ") * W) * (1_ G) is Element of the carrier of G
the multF of G . (((a ") * W),(1_ G)) is Element of the carrier of G
[((a ") * W),(1_ G)] is set
{((a ") * W),(1_ G)} is non empty set
{((a ") * W)} is non empty trivial 1 -element set
{{((a ") * W),(1_ G)},{((a ") * W)}} is non empty set
the multF of G . [((a ") * W),(1_ G)] is set
m " is Element of the carrier of G
m * (m ") is Element of the carrier of G
the multF of G . (m,(m ")) is Element of the carrier of G
[m,(m ")] is set
{m,(m ")} is non empty set
{m} is non empty trivial 1 -element set
{{m,(m ")},{m}} is non empty set
the multF of G . [m,(m ")] is set
((a ") * W) * (m * (m ")) is Element of the carrier of G
the multF of G . (((a ") * W),(m * (m "))) is Element of the carrier of G
[((a ") * W),(m * (m "))] is set
{((a ") * W),(m * (m "))} is non empty set
{{((a ") * W),(m * (m "))},{((a ") * W)}} is non empty set
the multF of G . [((a ") * W),(m * (m "))] is set
((a ") * W) * m is Element of the carrier of G
the multF of G . (((a ") * W),m) is Element of the carrier of G
[((a ") * W),m] is set
{((a ") * W),m} is non empty set
{{((a ") * W),m},{((a ") * W)}} is non empty set
the multF of G . [((a ") * W),m] is set
(((a ") * W) * m) * (m ") is Element of the carrier of G
the multF of G . ((((a ") * W) * m),(m ")) is Element of the carrier of G
[(((a ") * W) * m),(m ")] is set
{(((a ") * W) * m),(m ")} is non empty set
{(((a ") * W) * m)} is non empty trivial 1 -element set
{{(((a ") * W) * m),(m ")},{(((a ") * W) * m)}} is non empty set
the multF of G . [(((a ") * W) * m),(m ")] is set
(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 "),a},{(a ")}} is non empty set
the multF of G . [(a "),a] is set
((a ") * a) * (m ") is Element of the carrier of G
the multF of G . (((a ") * a),(m ")) is Element of the carrier of G
[((a ") * a),(m ")] is set
{((a ") * a),(m ")} is non empty set
{((a ") * a)} is non empty trivial 1 -element set
{{((a ") * a),(m ")},{((a ") * a)}} is non empty set
the multF of G . [((a ") * a),(m ")] is set
(1_ G) * (m ") is Element of the carrier of G
the multF of G . ((1_ G),(m ")) is Element of the carrier of G
[(1_ G),(m ")] is set
{(1_ G),(m ")} is non empty set
{{(1_ G),(m ")},{(1_ G)}} is non empty set
the multF of G . [(1_ G),(m ")] is set
(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),W},{(1_ G)}} is non empty set
the multF of G . [(1_ G),W] is set
r * (a ") is Element of bool the carrier of G
{(a ")} is non empty trivial 1 -element compact Element of bool the carrier of G
r * {(a ")} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in r & b2 in {(a ")} ) } is set
q is set
g is Element of the carrier of G
g * (a ") is Element of the carrier of G
the multF of G . (g,(a ")) is Element of the carrier of G
[g,(a ")] is set
{g,(a ")} is non empty set
{g} is non empty trivial 1 -element set
{{g,(a ")},{g}} is non empty set
the multF of G . [g,(a ")] is set
(r * (a ")) * W is Element of bool the carrier of G
(r * (a ")) * {W} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in r * (a ") & b2 in {W} ) } is set
(B * (W ")) * W is Element of bool the carrier of G
(B * (W ")) * {W} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B * (W ") & b2 in {W} ) } is set
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
(W ") * W is Element of the carrier of G
the multF of G . ((W "),W) is Element of the carrier of G
[(W "),W] is set
{(W "),W} is non empty set
{(W ")} is non empty trivial 1 -element set
{{(W "),W},{(W ")}} is non empty set
the multF of G . [(W "),W] is set
B * ((W ") * W) is Element of bool the carrier of G
{((W ") * W)} is non empty trivial 1 -element compact Element of bool the carrier of G
B * {((W ") * W)} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B & b2 in {((W ") * W)} ) } is set
B * (1_ G) is Element of bool the carrier of G
{(1_ G)} is non empty trivial 1 -element compact Element of bool the carrier of G
B * {(1_ G)} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B & b2 in {(1_ G)} ) } is set
bool the carrier of G is non empty Element of bool (bool the carrier of G)
B is set
p is Element of the carrier of G
W is Element of bool the carrier of G
W * p is Element of bool the carrier of G
{p} is non empty trivial 1 -element compact Element of bool the carrier of G
W * {p} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in W & b2 in {p} ) } is set
G is non empty TopSpace-like unital Group-like associative () () () ()
the carrier of G is non empty set
bool the carrier of G is non empty set
1_ G is non being_of_order_0 Element of the carrier of G
A is Element of bool the carrier of G
Int A is open Element of bool the carrier of G
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
(1_ G) " is Element of the carrier of G
(1_ G) * ((1_ G) ") 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:] 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 . ((1_ G),((1_ G) ")) is Element of the carrier of G
[(1_ G),((1_ G) ")] is set
{(1_ G),((1_ G) ")} is non empty set
{(1_ G)} is non empty trivial 1 -element set
{{(1_ G),((1_ G) ")},{(1_ G)}} is non empty set
the multF of G . [(1_ G),((1_ G) ")] is set
C is non empty open a_neighborhood of 1_ G
B is non empty open a_neighborhood of (1_ G) "
C * B is open Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in C & b2 in B ) } is set
((1_ G) ") " is Element of the carrier of G
B " is open Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in B } is set
C /\ (B ") is open Element of bool the carrier of G
W is non empty a_neighborhood of 1_ G
W " is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in W } is set
(B ") " is open Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in B " } is set
C * (W ") is open Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in C & b2 in W " ) } is set
Cl W is closed Element of bool the carrier of G
Int W is open Element of bool the carrier of G
W ` is Element of bool the carrier of G
the carrier of G \ W is set
Cl (W `) is closed Element of bool the carrier of G
(Cl (W `)) ` is open Element of bool the carrier of G
the carrier of G \ (Cl (W `)) is set
p is set
r is Element of the carrier of G
r * (1_ G) is Element of the carrier of G
the multF of G . (r,(1_ G)) is Element of the carrier of G
[r,(1_ G)] is set
{r,(1_ G)} is non empty set
{r} is non empty trivial 1 -element set
{{r,(1_ G)},{r}} is non empty set
the multF of G . [r,(1_ G)] is set
r * W is Element of bool the carrier of G
{r} is non empty trivial 1 -element compact Element of bool the carrier of G
{r} * W is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {r} & b2 in W ) } is set
(r * W) /\ W is Element of bool the carrier of G
a is set
a is Element of the carrier of G
b is Element of the carrier of G
r * b is Element of the carrier of G
the multF of G . (r,b) is Element of the carrier of G
[r,b] is set
{r,b} is non empty set
{{r,b},{r}} is non empty set
the multF of G . [r,b] is set
b " is Element of the carrier of G
b * (b ") is Element of the carrier of G
the multF of G . (b,(b ")) is Element of the carrier of G
[b,(b ")] is set
{b,(b ")} is non empty set
{b} is non empty trivial 1 -element set
{{b,(b ")},{b}} is non empty set
the multF of G . [b,(b ")] is set
r * (b * (b ")) is Element of the carrier of G
the multF of G . (r,(b * (b "))) is Element of the carrier of G
[r,(b * (b "))] is set
{r,(b * (b "))} is non empty set
{{r,(b * (b "))},{r}} is non empty set
the multF of G . [r,(b * (b "))] is set
a * (b ") is Element of the carrier of G
the multF of G . (a,(b ")) is Element of the carrier of G
[a,(b ")] is set
{a,(b ")} is non empty set
{a} is non empty trivial 1 -element set
{{a,(b ")},{a}} is non empty set
the multF of G . [a,(b ")] is set
e is Element of the carrier of G
G is non empty TopSpace-like unital Group-like associative () () () ()
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 V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]