:: 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