:: CONNSP_1 semantic presentation

K121() is set

K10(K121()) is non empty set

{} is empty V10() V11() V12() set

the empty V10() V11() V12() set is empty V10() V11() V12() set

1 is non empty set

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

Q is Element of K10( the carrier of G)

Cl Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

Cl C is Element of K10( the carrier of G)

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

(Cl P) /\ A is Element of K10( the carrier of G)

Cl A is Element of K10( the carrier of G)

P /\ (Cl A) is Element of K10( the carrier of G)

P /\ A is Element of K10( the carrier of G)

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P /\ A is Element of K10( the carrier of G)

Cl A is Element of K10( the carrier of G)

P /\ (Cl A) is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

(Cl P) /\ A is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

[#] G is non proper closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

([#] G) \ A is Element of K10( the carrier of G)

Cl (([#] G) \ A) is Element of K10( the carrier of G)

([#] G) \ P is Element of K10( the carrier of G)

Cl (([#] G) \ P) is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

[#] G is non proper closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

([#] G) \ A is Element of K10( the carrier of G)

Cl A is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

([#] G) \ P is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is TopSpace-like SubSpace of G

the carrier of P is set

K10( the carrier of P) is non empty set

A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of P)

F9 is Element of K10( the carrier of P)

Cl C is Element of K10( the carrier of P)

(Cl C) /\ F9 is Element of K10( the carrier of P)

Cl F9 is Element of K10( the carrier of P)

C /\ (Cl F9) is Element of K10( the carrier of P)

[#] P is non proper closed Element of K10( the carrier of P)

B is Element of K10( the carrier of G)

Cl B is Element of K10( the carrier of G)

([#] P) /\ (Cl B) is Element of K10( the carrier of G)

C /\ (([#] P) /\ (Cl B)) is Element of K10( the carrier of G)

C /\ ([#] P) is Element of K10( the carrier of P)

(C /\ ([#] P)) /\ (Cl B) is Element of K10( the carrier of G)

y is Element of K10( the carrier of G)

y /\ (Cl B) is Element of K10( the carrier of G)

Cl y is Element of K10( the carrier of G)

(Cl y) /\ ([#] P) is Element of K10( the carrier of P)

((Cl y) /\ ([#] P)) /\ F9 is Element of K10( the carrier of P)

F9 /\ ([#] P) is Element of K10( the carrier of P)

(Cl y) /\ (F9 /\ ([#] P)) is Element of K10( the carrier of P)

(Cl y) /\ B is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is TopSpace-like SubSpace of G

the carrier of P is set

K10( the carrier of P) is non empty set

[#] P is non proper closed Element of K10( the carrier of P)

A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

A \/ Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of P)

F9 is Element of K10( the carrier of P)

Cl A is Element of K10( the carrier of G)

(Cl A) /\ Q is Element of K10( the carrier of G)

Cl Q is Element of K10( the carrier of G)

A /\ (Cl Q) is Element of K10( the carrier of G)

y is Element of K10( the carrier of P)

B is Element of K10( the carrier of P)

Cl B is Element of K10( the carrier of P)

y /\ (Cl B) is Element of K10( the carrier of P)

([#] P) /\ (Cl Q) is Element of K10( the carrier of G)

y /\ (([#] P) /\ (Cl Q)) is Element of K10( the carrier of G)

y /\ ([#] P) is Element of K10( the carrier of P)

(y /\ ([#] P)) /\ (Cl Q) is Element of K10( the carrier of G)

Cl y is Element of K10( the carrier of P)

(Cl A) /\ ([#] P) is Element of K10( the carrier of P)

(Cl y) /\ B is Element of K10( the carrier of P)

B /\ ([#] P) is Element of K10( the carrier of P)

(Cl A) /\ (B /\ ([#] P)) is Element of K10( the carrier of P)

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

(Cl P) /\ A is Element of K10( the carrier of G)

Cl A is Element of K10( the carrier of G)

P /\ (Cl A) is Element of K10( the carrier of G)

Cl C is Element of K10( the carrier of G)

Q /\ (Cl C) is Element of K10( the carrier of G)

{} G is empty V10() V11() V12() Element of K10( the carrier of G)

Cl Q is Element of K10( the carrier of G)

(Cl Q) /\ C is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

A \/ Q is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

Cl A is Element of K10( the carrier of G)

Cl Q is Element of K10( the carrier of G)

P /\ (Cl A) is Element of K10( the carrier of G)

Cl (A \/ Q) is Element of K10( the carrier of G)

P /\ (Cl (A \/ Q)) is Element of K10( the carrier of G)

(Cl A) \/ (Cl Q) is Element of K10( the carrier of G)

P /\ ((Cl A) \/ (Cl Q)) is Element of K10( the carrier of G)

P /\ (Cl Q) is Element of K10( the carrier of G)

(P /\ (Cl A)) \/ (P /\ (Cl Q)) is Element of K10( the carrier of G)

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

(Cl P) /\ A is Element of K10( the carrier of G)

(Cl P) /\ (A \/ Q) is Element of K10( the carrier of G)

(Cl P) /\ Q is Element of K10( the carrier of G)

((Cl P) /\ A) \/ ((Cl P) /\ Q) is Element of K10( the carrier of G)

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \ A is Element of K10( the carrier of G)

A \ P is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

C ` is Element of K10( the carrier of G)

the carrier of G \ C is set

Q /\ (C `) is Element of K10( the carrier of G)

Cl C is Element of K10( the carrier of G)

Q ` is Element of K10( the carrier of G)

the carrier of G \ Q is set

(Cl C) /\ (Q `) is Element of K10( the carrier of G)

[#] G is non proper Element of K10( the carrier of G)

([#] G) \ Q is Element of K10( the carrier of G)

Cl (([#] G) \ Q) is Element of K10( the carrier of G)

Cl (Q `) is Element of K10( the carrier of G)

(Cl C) /\ (Cl (Q `)) is Element of K10( the carrier of G)

(Q /\ (C `)) /\ ((Cl C) /\ (Cl (Q `))) is Element of K10( the carrier of G)

Q /\ (Q `) is Element of K10( the carrier of G)

Q \ C is Element of K10( the carrier of G)

C /\ (Q `) is Element of K10( the carrier of G)

Cl Q is Element of K10( the carrier of G)

(Cl Q) /\ (C `) is Element of K10( the carrier of G)

((Cl Q) /\ (C `)) /\ (C /\ (Q `)) is Element of K10( the carrier of G)

C /\ (C `) is Element of K10( the carrier of G)

Cl (C `) is Element of K10( the carrier of G)

(Cl Q) /\ (Cl (C `)) is Element of K10( the carrier of G)

((Cl Q) /\ (Cl (C `))) /\ (C /\ (Q `)) is Element of K10( the carrier of G)

C \ Q is Element of K10( the carrier of G)

Cl (C /\ (Q `)) is Element of K10( the carrier of G)

Cl (C \ Q) is Element of K10( the carrier of G)

(Q \ C) /\ (Cl (C \ Q)) is Element of K10( the carrier of G)

{} G is empty V10() V11() V12() Element of K10( the carrier of G)

Cl (Q /\ (C `)) is Element of K10( the carrier of G)

Cl (Q \ C) is Element of K10( the carrier of G)

(Cl (Q \ C)) /\ (C \ Q) is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

([#] G) \ C is Element of K10( the carrier of G)

([#] G) \ Q is Element of K10( the carrier of G)

(([#] G) \ Q) \ (([#] G) \ C) is Element of K10( the carrier of G)

Q ` is Element of K10( the carrier of G)

the carrier of G \ Q is set

(([#] G) \ C) ` is Element of K10( the carrier of G)

the carrier of G \ (([#] G) \ C) is set

(Q `) /\ ((([#] G) \ C) `) is Element of K10( the carrier of G)

(Q `) /\ C is Element of K10( the carrier of G)

C \ Q is Element of K10( the carrier of G)

(([#] G) \ C) \ (([#] G) \ Q) is Element of K10( the carrier of G)

C ` is Element of K10( the carrier of G)

the carrier of G \ C is set

(([#] G) \ Q) ` is Element of K10( the carrier of G)

the carrier of G \ (([#] G) \ Q) is set

(C `) /\ ((([#] G) \ Q) `) is Element of K10( the carrier of G)

(C `) /\ Q is Element of K10( the carrier of G)

Q \ C is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

[#] G is non proper closed Element of K10( the carrier of G)

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

Q \/ C is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

[#] G is non proper closed Element of K10( the carrier of G)

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

Q \/ C is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

[#] G is non proper closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

([#] G) \ P is Element of K10( the carrier of G)

Cl (([#] G) \ P) is Element of K10( the carrier of G)

(Cl P) /\ (Cl (([#] G) \ P)) is Element of K10( the carrier of G)

P /\ (Cl (([#] G) \ P)) is Element of K10( the carrier of G)

P ` is Element of K10( the carrier of G)

the carrier of G \ P is set

P \/ (P `) is Element of K10( the carrier of G)

(Cl P) /\ (([#] G) \ P) is Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

Cl A is Element of K10( the carrier of G)

([#] G) \ P is Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

([#] G) \ P is Element of K10( the carrier of G)

Cl (([#] G) \ P) is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

Cl A is Element of K10( the carrier of G)

([#] G) \ A is Element of K10( the carrier of G)

Cl (([#] G) \ A) is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

[#] G is non proper closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

([#] G) \ Q is Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

([#] G) \ P is Element of K10( the carrier of G)

Cl (([#] G) \ P) is Element of K10( the carrier of G)

P ` is Element of K10( the carrier of G)

the carrier of G \ P is set

Cl P is Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

[#] G is non proper closed Element of K10( the carrier of G)

K10( the carrier of G) is non empty set

P is TopSpace-like TopStruct

the carrier of P is set

K11( the carrier of G, the carrier of P) is V10() set

K10(K11( the carrier of G, the carrier of P)) is non empty set

[#] P is non proper closed Element of K10( the carrier of P)

K10( the carrier of P) is non empty set

A is V10() V13( the carrier of G) V14( the carrier of P) V15() V21( the carrier of G, the carrier of P) Element of K10(K11( the carrier of G, the carrier of P))

A .: ([#] G) is Element of K10( the carrier of P)

{} P is empty V10() V11() V12() closed Element of K10( the carrier of P)

Q is Element of K10( the carrier of P)

C is Element of K10( the carrier of P)

Q \/ C is Element of K10( the carrier of P)

A " Q is Element of K10( the carrier of G)

A " C is Element of K10( the carrier of G)

Q /\ C is Element of K10( the carrier of P)

(A " Q) /\ (A " C) is Element of K10( the carrier of G)

A " (Q /\ C) is Element of K10( the carrier of G)

A " the carrier of P is Element of K10( the carrier of G)

(A " Q) \/ (A " C) is Element of K10( the carrier of G)

rng A is Element of K10( the carrier of P)

A .: the carrier of G is Element of K10( the carrier of P)

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

G | P is strict TopSpace-like SubSpace of G

[#] (G | P) is non proper closed Element of K10( the carrier of (G | P))

the carrier of (G | P) is set

K10( the carrier of (G | P)) is non empty set

{} (G | P) is empty V10() V11() V12() closed Element of K10( the carrier of (G | P))

A is Element of K10( the carrier of (G | P))

Q is Element of K10( the carrier of (G | P))

A \/ Q is Element of K10( the carrier of (G | P))

F9 is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

A \/ Q is Element of K10( the carrier of G)

F9 is Element of K10( the carrier of (G | P))

C is Element of K10( the carrier of (G | P))

A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

A \/ Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

F9 is Element of K10( the carrier of G)

C \/ F9 is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

A \/ Q is Element of K10( the carrier of G)

P /\ Q is Element of K10( the carrier of G)

P /\ A is Element of K10( the carrier of G)

(P /\ A) \/ (P /\ Q) is Element of K10( the carrier of G)

P /\ (A \/ Q) is Element of K10( the carrier of G)

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

Q \/ C is Element of K10( the carrier of G)

Q /\ C is Element of K10( the carrier of G)

C \/ Q is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

Q \/ C is Element of K10( the carrier of G)

Cl C is Element of K10( the carrier of G)

Q /\ (Cl C) is Element of K10( the carrier of G)

Q /\ (Cl P) is Element of K10( the carrier of G)

Q /\ A is Element of K10( the carrier of G)

Cl Q is Element of K10( the carrier of G)

(Cl Q) /\ C is Element of K10( the carrier of G)

(Cl P) /\ C is Element of K10( the carrier of G)

A /\ C is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

[#] G is non proper closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

([#] G) \ P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

A \/ Q is Element of K10( the carrier of G)

P \/ Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

([#] G) \ C is Element of K10( the carrier of G)

F9 is Element of K10( the carrier of G)

y is Element of K10( the carrier of G)

F9 \/ y is Element of K10( the carrier of G)

C \/ F9 is Element of K10( the carrier of G)

B is Element of K10( the carrier of G)

B is Element of K10( the carrier of G)

B \/ B is Element of K10( the carrier of G)

C \/ (F9 \/ y) is Element of K10( the carrier of G)

(B \/ B) \/ y is Element of K10( the carrier of G)

B \/ y is Element of K10( the carrier of G)

B \/ (B \/ y) is Element of K10( the carrier of G)

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

B \/ y is Element of K10( the carrier of G)

B \/ (B \/ y) is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

[#] G is non proper closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

([#] G) \ P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

A \/ Q is Element of K10( the carrier of G)

P \/ Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

([#] G) \ C is Element of K10( the carrier of G)

F9 is Element of K10( the carrier of G)

y is Element of K10( the carrier of G)

F9 \/ y is Element of K10( the carrier of G)

Cl C is Element of K10( the carrier of G)

Cl F9 is Element of K10( the carrier of G)

(Cl F9) /\ y is Element of K10( the carrier of G)

C \/ (F9 \/ y) is Element of K10( the carrier of G)

C \/ F9 is Element of K10( the carrier of G)

Cl (C \/ F9) is Element of K10( the carrier of G)

(Cl C) \/ (Cl F9) is Element of K10( the carrier of G)

(Cl F9) /\ (C \/ (F9 \/ y)) is Element of K10( the carrier of G)

C \/ ((Cl F9) /\ (C \/ (F9 \/ y))) is Element of K10( the carrier of G)

C \/ (Cl F9) is Element of K10( the carrier of G)

C \/ (C \/ (F9 \/ y)) is Element of K10( the carrier of G)

(C \/ (Cl F9)) /\ (C \/ (C \/ (F9 \/ y))) is Element of K10( the carrier of G)

C \/ C is Element of K10( the carrier of G)

(C \/ C) \/ (F9 \/ y) is Element of K10( the carrier of G)

(C \/ (Cl F9)) /\ ((C \/ C) \/ (F9 \/ y)) is Element of K10( the carrier of G)

(Cl F9) /\ (F9 \/ y) is Element of K10( the carrier of G)

C \/ ((Cl F9) /\ (F9 \/ y)) is Element of K10( the carrier of G)

(Cl F9) /\ F9 is Element of K10( the carrier of G)

((Cl F9) /\ F9) \/ ((Cl F9) /\ y) is Element of K10( the carrier of G)

C \/ (((Cl F9) /\ F9) \/ ((Cl F9) /\ y)) is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \ A is Element of K10( the carrier of G)

Fr A is Element of K10( the carrier of G)

A ` is Element of K10( the carrier of G)

the carrier of G \ A is set

Cl (A `) is Element of K10( the carrier of G)

P /\ A is Element of K10( the carrier of G)

Cl (P /\ A) is Element of K10( the carrier of G)

Cl A is Element of K10( the carrier of G)

(Cl (P /\ A)) /\ (A `) is Element of K10( the carrier of G)

(Cl A) /\ (Cl (A `)) is Element of K10( the carrier of G)

P /\ (A `) is Element of K10( the carrier of G)

Cl (P \ A) is Element of K10( the carrier of G)

Cl (P /\ (A `)) is Element of K10( the carrier of G)

A /\ (Cl (P /\ (A `))) is Element of K10( the carrier of G)

((Cl (P /\ A)) /\ (A `)) \/ (A /\ (Cl (P /\ (A `)))) is Element of K10( the carrier of G)

P /\ (((Cl (P /\ A)) /\ (A `)) \/ (A /\ (Cl (P /\ (A `))))) is Element of K10( the carrier of G)

P /\ ((Cl A) /\ (Cl (A `))) is Element of K10( the carrier of G)

[#] G is non proper closed Element of K10( the carrier of G)

P /\ ([#] G) is Element of K10( the carrier of G)

A \/ (A `) is Element of K10( the carrier of G)

P /\ (A \/ (A `)) is Element of K10( the carrier of G)

(P /\ A) \/ (P \ A) is Element of K10( the carrier of G)

(Cl (P /\ A)) /\ (P \ A) is Element of K10( the carrier of G)

(P /\ A) /\ (Cl (P \ A)) is Element of K10( the carrier of G)

((Cl (P /\ A)) /\ (P \ A)) \/ ((P /\ A) /\ (Cl (P \ A))) is Element of K10( the carrier of G)

(Cl (P /\ A)) /\ P is Element of K10( the carrier of G)

((Cl (P /\ A)) /\ P) /\ (A `) is Element of K10( the carrier of G)

(P /\ A) /\ (Cl (P /\ (A `))) is Element of K10( the carrier of G)

(((Cl (P /\ A)) /\ P) /\ (A `)) \/ ((P /\ A) /\ (Cl (P /\ (A `)))) is Element of K10( the carrier of G)

P /\ (Cl (P /\ A)) is Element of K10( the carrier of G)

(P /\ (Cl (P /\ A))) /\ (A `) is Element of K10( the carrier of G)

P /\ (A /\ (Cl (P /\ (A `)))) is Element of K10( the carrier of G)

((P /\ (Cl (P /\ A))) /\ (A `)) \/ (P /\ (A /\ (Cl (P /\ (A `))))) is Element of K10( the carrier of G)

P /\ ((Cl (P /\ A)) /\ (A `)) is Element of K10( the carrier of G)

(P /\ ((Cl (P /\ A)) /\ (A `))) \/ (P /\ (A /\ (Cl (P /\ (A `))))) is Element of K10( the carrier of G)

P /\ (Fr A) is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is TopSpace-like SubSpace of G

the carrier of P is set

K10( the carrier of P) is non empty set

A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of P)

G | A is strict TopSpace-like SubSpace of G

[#] (G | A) is non proper closed Element of K10( the carrier of (G | A))

the carrier of (G | A) is set

K10( the carrier of (G | A)) is non empty set

F9 is TopSpace-like TopStruct

the carrier of F9 is set

K10( the carrier of F9) is non empty set

C is TopSpace-like TopStruct

the carrier of C is set

K10( the carrier of C) is non empty set

P | Q is strict TopSpace-like SubSpace of P

[#] (P | Q) is non proper closed Element of K10( the carrier of (P | Q))

the carrier of (P | Q) is set

K10( the carrier of (P | Q)) is non empty set

{} (G | A) is empty V10() V11() V12() closed Element of K10( the carrier of (G | A))

{} (P | Q) is empty V10() V11() V12() closed Element of K10( the carrier of (P | Q))

B is Element of K10( the carrier of C)

C | B is strict TopSpace-like SubSpace of C

B is Element of K10( the carrier of (G | A))

Q is Element of K10( the carrier of (G | A))

B \/ Q is Element of K10( the carrier of (G | A))

QQ is Element of K10( the carrier of G)

QQ /\ ([#] (G | A)) is Element of K10( the carrier of (G | A))

[#] P is non proper closed Element of K10( the carrier of P)

QQ /\ ([#] P) is Element of K10( the carrier of P)

PP is Element of K10( the carrier of P)

QQ /\ A is Element of K10( the carrier of G)

(QQ /\ ([#] P)) /\ A is Element of K10( the carrier of G)

PP /\ ([#] (P | Q)) is Element of K10( the carrier of (P | Q))

P1 is Element of K10( the carrier of (P | Q))

Q2 is Element of K10( the carrier of G)

Q2 /\ ([#] (G | A)) is Element of K10( the carrier of (G | A))

Q2 /\ ([#] P) is Element of K10( the carrier of P)

Q2 /\ A is Element of K10( the carrier of G)

(Q2 /\ ([#] P)) /\ A is Element of K10( the carrier of G)

P2 is Element of K10( the carrier of P)

Q1 is Element of K10( the carrier of (P | Q))

y is Element of K10( the carrier of F9)

F9 | y is strict TopSpace-like SubSpace of F9

B is Element of K10( the carrier of (P | Q))

Q is Element of K10( the carrier of (P | Q))

B \/ Q is Element of K10( the carrier of (P | Q))

P1 is Element of K10( the carrier of P)

P1 /\ ([#] (P | Q)) is Element of K10( the carrier of (P | Q))

Q1 is Element of K10( the carrier of P)

Q1 /\ ([#] (P | Q)) is Element of K10( the carrier of (P | Q))

Q2 is Element of K10( the carrier of G)

Q2 /\ ([#] P) is Element of K10( the carrier of P)

Q2 /\ ([#] (G | A)) is Element of K10( the carrier of (G | A))

([#] P) /\ Q is Element of K10( the carrier of P)

Q2 /\ (([#] P) /\ Q) is Element of K10( the carrier of P)

QQ is Element of K10( the carrier of (G | A))

P2 is Element of K10( the carrier of G)

P2 /\ ([#] P) is Element of K10( the carrier of P)

P2 /\ ([#] (G | A)) is Element of K10( the carrier of (G | A))

P2 /\ (([#] P) /\ Q) is Element of K10( the carrier of P)

PP is Element of K10( the carrier of (G | A))

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

P /\ A is Element of K10( the carrier of G)

G | (P \/ A) is strict TopSpace-like SubSpace of G

[#] (G | (P \/ A)) is non proper closed Element of K10( the carrier of (G | (P \/ A)))

the carrier of (G | (P \/ A)) is set

K10( the carrier of (G | (P \/ A))) is non empty set

F9 is Element of K10( the carrier of (G | (P \/ A)))

C is Element of K10( the carrier of (G | (P \/ A)))

F9 /\ C is Element of K10( the carrier of (G | (P \/ A)))

([#] (G | (P \/ A))) \ (F9 /\ C) is Element of K10( the carrier of (G | (P \/ A)))

F9 \ C is Element of K10( the carrier of (G | (P \/ A)))

C \ F9 is Element of K10( the carrier of (G | (P \/ A)))

(F9 \ C) \/ (C \ F9) is Element of K10( the carrier of (G | (P \/ A)))

A /\ ([#] (G | (P \/ A))) is Element of K10( the carrier of (G | (P \/ A)))

P /\ ([#] (G | (P \/ A))) is Element of K10( the carrier of (G | (P \/ A)))

(F9 /\ C) \/ (C \ F9) is Element of K10( the carrier of (G | (P \/ A)))

(F9 /\ C) \/ (F9 \ C) is Element of K10( the carrier of (G | (P \/ A)))

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

K10(K10( the carrier of G)) is non empty set

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

P is Element of K10(K10( the carrier of G))

union P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

F9 is Element of K10( the carrier of G)

C \/ F9 is Element of K10( the carrier of G)

C /\ F9 is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

y is Element of K10( the carrier of G)

y is set

y is Element of K10( the carrier of G)

y is set

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

K10(K10( the carrier of G)) is non empty set

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

P is Element of K10(K10( the carrier of G))

meet P is Element of K10( the carrier of G)

union P is Element of K10( the carrier of G)

A is Element of the carrier of G

Q is set

F9 is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

Cl C is Element of K10( the carrier of G)

Cl F9 is Element of K10( the carrier of G)

(Cl C) /\ F9 is Element of K10( the carrier of G)

C /\ (Cl F9) is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

[#] G is non proper closed Element of K10( the carrier of G)

the carrier of G is set

K10( the carrier of G) is non empty set

G | ([#] G) is strict TopSpace-like SubSpace of G

[#] (G | ([#] G)) is non proper closed Element of K10( the carrier of (G | ([#] G)))

the carrier of (G | ([#] G)) is set

K10( the carrier of (G | ([#] G))) is non empty set

{} (G | ([#] G)) is empty V10() V11() V12() closed Element of K10( the carrier of (G | ([#] G)))

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

P is Element of K10( the carrier of (G | ([#] G)))

A is Element of K10( the carrier of (G | ([#] G)))

P \/ A is Element of K10( the carrier of (G | ([#] G)))

C is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

C is Element of K10( the carrier of (G | ([#] G)))

Q is Element of K10( the carrier of (G | ([#] G)))

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

K10( the carrier of G) is non empty set

P is Element of the carrier of G

{P} is non empty Element of K10( the carrier of G)

{} G is empty proper V10() V11() V12() closed Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

A \/ Q is Element of K10( the carrier of G)

A /\ Q is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

G is TopStruct

the carrier of G is set

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

P is Element of the carrier of G

K10( the carrier of G) is non empty set

A is Element of the carrier of G

K10(K10( the carrier of G)) is non empty set

Q is Element of K10(K10( the carrier of G))

F9 is Element of K10( the carrier of G)

C is Element of K10(K10( the carrier of G))

y is Element of K10( the carrier of G)

A is Element of K10(K10( the carrier of G))

Q is Element of the carrier of G

Q is set

[#] G is non empty non proper closed Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

union A is Element of K10( the carrier of G)

Q is set

{P} is non empty (G) Element of K10( the carrier of G)

meet A is Element of K10( the carrier of G)

{} G is empty proper V10() V11() V12() closed Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

P is Element of the carrier of G

A is Element of the carrier of G

K10( the carrier of G) is non empty set

C is Element of K10( the carrier of G)

Q is Element of the carrier of G

F9 is Element of K10( the carrier of G)

C /\ F9 is Element of K10( the carrier of G)

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

C \/ F9 is Element of K10( the carrier of G)

the Element of the carrier of G is Element of the carrier of G

A is Element of the carrier of G

P is Element of the carrier of G

A is Element of the carrier of G

Q is Element of the carrier of G

C is Element of the carrier of G

F9 is Element of the carrier of G

y is Element of the carrier of G

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

P is Element of the carrier of G

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

K10( the carrier of G) is non empty set

K10(K10( the carrier of G)) is non empty set

P is Element of the carrier of G

A is Element of K10(K10( the carrier of G))

{P} is non empty (G) Element of K10( the carrier of G)

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

K10( the carrier of G) is non empty set

the Element of the carrier of G is Element of the carrier of G

{ the Element of the carrier of G} is non empty (G) Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

{} G is empty proper V10() V11() V12() closed Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

Cl P is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

P \/ A is Element of K10( the carrier of G)

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

[#] G is non proper closed Element of K10( the carrier of G)

P is Element of K10( the carrier of G)

([#] G) \ P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

([#] G) \ A is Element of K10( the carrier of G)

G | (([#] G) \ P) is strict TopSpace-like SubSpace of G

the carrier of (G | (([#] G) \ P)) is set

K10( the carrier of (G | (([#] G) \ P))) is non empty set

Q is Element of K10( the carrier of (G | (([#] G) \ P)))

[#] (G | (([#] G) \ P)) is non proper closed Element of K10( the carrier of (G | (([#] G) \ P)))

(([#] G) \ P) ` is Element of K10( the carrier of G)

the carrier of G \ (([#] G) \ P) is set

C is Element of K10( the carrier of G)

C ` is Element of K10( the carrier of G)

the carrier of G \ C is set

P /\ Q is Element of K10( the carrier of (G | (([#] G) \ P)))

F9 is Element of K10( the carrier of G)

y is Element of K10( the carrier of G)

F9 \/ y is Element of K10( the carrier of G)

F9 ` is Element of K10( the carrier of G)

the carrier of G \ F9 is set

y ` is Element of K10( the carrier of G)

the carrier of G \ y is set

P /\ F9 is Element of K10( the carrier of G)

y /\ (y `) is Element of K10( the carrier of G)

A \/ F9 is Element of K10( the carrier of G)

(A \/ F9) /\ P is Element of K10( the carrier of G)

P /\ A is Element of K10( the carrier of G)

(P /\ A) \/ (P /\ F9) is Element of K10( the carrier of G)

P ` is Element of K10( the carrier of G)

the carrier of G \ P is set

A ` is Element of K10( the carrier of G)

the carrier of G \ A is set

B is Element of K10( the carrier of (G | (([#] G) \ P)))

Q \/ F9 is set

A /\ (([#] G) \ A) is Element of K10( the carrier of G)

{} G is empty V10() V11() V12() closed Element of K10( the carrier of G)

P /\ y is Element of K10( the carrier of G)

F9 /\ (F9 `) is Element of K10( the carrier of G)

A \/ y is Element of K10( the carrier of G)

(A \/ y) /\ P is Element of K10( the carrier of G)

(P /\ A) \/ (P /\ y) is Element of K10( the carrier of G)

B is Element of K10( the carrier of (G | (([#] G) \ P)))

Q \/ y is set

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

K10(K10( the carrier of G)) is non empty set

P is Element of the carrier of G

A is Element of K10(K10( the carrier of G))

union A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10(K10( the carrier of G))

union C is Element of K10( the carrier of G)

C is Element of K10(K10( the carrier of G))

union C is Element of K10( the carrier of G)

F9 is Element of K10(K10( the carrier of G))

union F9 is Element of K10( the carrier of G)

F9 is Element of K10(K10( the carrier of G))

union F9 is Element of K10( the carrier of G)

y is set

B is set

B is Element of K10( the carrier of G)

B is set

B is Element of K10( the carrier of G)

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

P is Element of the carrier of G

(G,P) is Element of K10( the carrier of G)

K10( the carrier of G) is non empty set

K10(K10( the carrier of G)) is non empty set

A is Element of K10(K10( the carrier of G))

union A is Element of K10( the carrier of G)

Q is set

meet A is Element of K10( the carrier of G)

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

P is Element of the carrier of G

(G,P) is Element of K10( the carrier of G)

K10( the carrier of G) is non empty set

K10(K10( the carrier of G)) is non empty set

A is Element of K10(K10( the carrier of G))

union A is Element of K10( the carrier of G)

Q is set

meet A is Element of K10( the carrier of G)

{} G is empty proper V10() V11() V12() closed Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of the carrier of G

(G,A) is non empty (G) Element of K10( the carrier of G)

K10(K10( the carrier of G)) is non empty set

Q is Element of K10(K10( the carrier of G))

union Q is Element of K10( the carrier of G)

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

{} G is empty proper V10() V11() V12() closed Element of K10( the carrier of G)

A is Element of the carrier of G

K10(K10( the carrier of G)) is non empty set

Q is Element of the carrier of G

(G,Q) is non empty (G) Element of K10( the carrier of G)

C is Element of K10(K10( the carrier of G))

union C is Element of K10( the carrier of G)

A is Element of the carrier of G

(G,A) is non empty (G) Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of the carrier of G

(G,A) is non empty (G) Element of K10( the carrier of G)

P /\ (G,A) is Element of K10( the carrier of G)

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

P is Element of the carrier of G

(G,P) is non empty (G) Element of K10( the carrier of G)

K10( the carrier of G) is non empty set

Q is Element of the carrier of G

(G,Q) is non empty (G) Element of K10( the carrier of G)

(G,Q) /\ (G,P) is Element of K10( the carrier of G)

{} G is empty proper V10() V11() V12() closed Element of K10( the carrier of G)

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

K10( the carrier of G) is non empty set

K10(K10( the carrier of G)) is non empty set

P is Element of K10(K10( the carrier of G))

A is set

[#] G is non empty non proper closed Element of K10( the carrier of G)

Q is Element of the carrier of G

(G,Q) is non empty (G) Element of K10( the carrier of G)

union P is Element of K10( the carrier of G)

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

{} G is empty V10() V11() V12() Element of K10( the carrier of G)

G is TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

G | P is strict SubSpace of G

the carrier of (G | P) is set

K10( the carrier of (G | P)) is non empty set

[#] (G | P) is non proper Element of K10( the carrier of (G | P))

Q is Element of K10( the carrier of (G | P))

C is Element of K10( the carrier of (G | P))

Q \/ C is Element of K10( the carrier of (G | P))

{} (G | P) is empty V10() V11() V12() Element of K10( the carrier of (G | P))

A is empty V10() V11() V12() Element of K10( the carrier of G)

G | A is empty V45() V46() V51( {} ) strict T_0 SubSpace of G

[#] (G | A) is empty V2() non proper V10() V11() V12() Element of K10( the carrier of (G | A))

the carrier of (G | A) is empty V2() V10() V11() V12() V31() set

K10( the carrier of (G | A)) is non empty set

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

the topology of G is non empty Element of K10(K10( the carrier of G))

K10(K10( the carrier of G)) is non empty set

TopStruct(# the carrier of G, the topology of G #) is strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of G, the topology of G #) is set

K10( the carrier of TopStruct(# the carrier of G, the topology of G #)) is non empty set

P is set

A is Element of K10( the carrier of G)

G | A is strict TopSpace-like SubSpace of G

the carrier of (G | A) is set

the topology of (G | A) is non empty Element of K10(K10( the carrier of (G | A)))

K10( the carrier of (G | A)) is non empty set

K10(K10( the carrier of (G | A))) is non empty set

TopStruct(# the carrier of (G | A), the topology of (G | A) #) is strict TopSpace-like TopStruct

Q is Element of K10( the carrier of TopStruct(# the carrier of G, the topology of G #))

TopStruct(# the carrier of G, the topology of G #) | Q is strict TopSpace-like SubSpace of TopStruct(# the carrier of G, the topology of G #)

A is Element of K10( the carrier of TopStruct(# the carrier of G, the topology of G #))

Q is Element of K10( the carrier of G)

G | Q is strict TopSpace-like SubSpace of G

the carrier of (G | Q) is set

the topology of (G | Q) is non empty Element of K10(K10( the carrier of (G | Q)))

K10( the carrier of (G | Q)) is non empty set

K10(K10( the carrier of (G | Q))) is non empty set

TopStruct(# the carrier of (G | Q), the topology of (G | Q) #) is strict TopSpace-like TopStruct

TopStruct(# the carrier of G, the topology of G #) | A is strict TopSpace-like SubSpace of TopStruct(# the carrier of G, the topology of G #)

G is TopSpace-like TopStruct

the carrier of G is set

K10( the carrier of G) is non empty set

the topology of G is non empty Element of K10(K10( the carrier of G))

K10(K10( the carrier of G)) is non empty set

TopStruct(# the carrier of G, the topology of G #) is strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of G, the topology of G #) is set

K10( the carrier of TopStruct(# the carrier of G, the topology of G #)) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of TopStruct(# the carrier of G, the topology of G #))

Q is Element of K10( the carrier of TopStruct(# the carrier of G, the topology of G #))

C is Element of K10( the carrier of G)

Q is Element of K10( the carrier of G)

C is Element of K10( the carrier of TopStruct(# the carrier of G, the topology of G #))

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

K10( the carrier of G) is non empty set

P is Element of K10( the carrier of G)

A is Element of K10( the carrier of G)

G | A is strict TopSpace-like SubSpace of G

the carrier of (G | A) is set

K10( the carrier of (G | A)) is non empty set

Q is Element of K10( the carrier of (G | A))

G | P is strict TopSpace-like SubSpace of G

(G | A) | Q is strict TopSpace-like SubSpace of G | A