:: TOPGRP_1 semantic presentation

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

{ (b

B is Element of bool the carrier of G

A * B is Element of bool the carrier of G

{ (b

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

{ (b

A * C is Element of bool the carrier of G

A * {C} is Element of bool the carrier of G

{ (b

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

{ (b

C * A is Element of bool the carrier of G

{C} * A is Element of bool the carrier of G

{ (b

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

{ (b

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

{ (b

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

{ (b

A is Element of bool the carrier of G

A " is Element of bool the carrier of G

{ (b

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

{ (b

A is Element of bool the carrier of G

A " is Element of bool the carrier of G

{ (b

(e ") " is Element of bool the carrier of G

{ (b

(A ") " is Element of bool the carrier of G

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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