:: TOPGEN_1 semantic presentation

omega is ordinal non finite cardinal limit_cardinal set
K10(omega) is non empty non finite set
REAL is set
K10(REAL) is non empty set
NAT is ordinal non finite cardinal limit_cardinal Element of K10(REAL)
K200() is V114() TopStruct
the carrier of K200() is set
1 is non empty set
K11(1,1) is non empty set
K10(K11(1,1)) is non empty set
K11(K11(1,1),1) is non empty set
K10(K11(K11(1,1),1)) is non empty set
K11(K11(1,1),REAL) is set
K10(K11(K11(1,1),REAL)) is non empty set
K11(REAL,REAL) is set
K11(K11(REAL,REAL),REAL) is set
K10(K11(K11(REAL,REAL),REAL)) is non empty set
2 is non empty set
K11(2,2) is non empty set
K11(K11(2,2),REAL) is set
K10(K11(K11(2,2),REAL)) is non empty set
K228() is V100() V114() L7()
R^1 is non empty strict TopSpace-like V114() TopStruct
{} is set
the empty ordinal cardinal {} -element set is empty ordinal cardinal {} -element set
the carrier of R^1 is non empty set
K10( the carrier of R^1) is non empty set
RAT is set
IRRAT is Element of K10(REAL)
REAL \ RAT is Element of K10(REAL)
B is 1-sorted
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
B ` is Element of K10( the carrier of B)
the carrier of B \ B is set
A \ B is Element of K10( the carrier of B)
A /\ (B `) is Element of K10( the carrier of B)
B is 1-sorted
[#] B is non proper Element of K10( the carrier of B)
the carrier of B is set
K10( the carrier of B) is non empty set
card ([#] B) is ordinal cardinal set
B is finite 1-sorted
[#] B is non proper Element of K10( the carrier of B)
the carrier of B is finite set
K10( the carrier of B) is non empty set
B is 1-sorted
the carrier of B is set
the non empty finite countable 1-sorted is non empty finite countable 1-sorted
the non empty finite TopSpace-like countable TopStruct is non empty finite TopSpace-like countable TopStruct
B is countable 1-sorted
[#] B is non proper Element of K10( the carrier of B)
the carrier of B is set
K10( the carrier of B) is non empty set
the non empty TopSpace-like T_1 T_2 V64() normal discrete TopStruct is non empty TopSpace-like T_1 T_2 V64() normal discrete TopStruct
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
Int A is open Element of K10( the carrier of B)
A ` is Element of K10( the carrier of B)
the carrier of B \ A is set
Cl (A `) is closed Element of K10( the carrier of B)
(Cl (A `)) ` is open Element of K10( the carrier of B)
the carrier of B \ (Cl (A `)) is set
(A `) ` is Element of K10( the carrier of B)
the carrier of B \ (A `) is set
((A `) `) ` is Element of K10( the carrier of B)
the carrier of B \ ((A `) `) is set
Cl (((A `) `) `) is closed Element of K10( the carrier of B)
(Cl (((A `) `) `)) ` is open Element of K10( the carrier of B)
the carrier of B \ (Cl (((A `) `) `)) is set
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
B is Element of K10(K10( the carrier of B))
A is Element of K10(K10( the carrier of B))
c<sub>5</sub> is set
B is Element of K10( the carrier of B)
q is Element of K10( the carrier of B)
Fr q is closed Element of K10( the carrier of B)
c<sub>5</sub> is set
B is Element of K10( the carrier of B)
Fr B is closed Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
(B,A) is Element of K10(K10( the carrier of B))
B is set
A is Element of K10( the carrier of B)
Fr A is closed Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
(B,A) is Element of K10(K10( the carrier of B))
B is Element of K10( the carrier of B)
{B} is non empty V2() 1 -element Element of K10(K10( the carrier of B))
Fr B is closed Element of K10( the carrier of B)
{(Fr B)} is non empty V2() 1 -element Element of K10(K10( the carrier of B))
A is set
c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
Fr B is closed Element of K10( the carrier of B)
A is set
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
B is Element of K10(K10( the carrier of B))
(B,A) is Element of K10(K10( the carrier of B))
(B,B) is Element of K10(K10( the carrier of B))
A is set
c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
Fr B is closed Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
B is Element of K10(K10( the carrier of B))
A \/ B is Element of K10(K10( the carrier of B))
(B,(A \/ B)) is Element of K10(K10( the carrier of B))
(B,A) is Element of K10(K10( the carrier of B))
(B,B) is Element of K10(K10( the carrier of B))
(B,A) \/ (B,B) is Element of K10(K10( the carrier of B))
A is set
c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
Fr B is closed Element of K10( the carrier of B)
B is TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
Fr A is Element of K10( the carrier of B)
Cl A is Element of K10( the carrier of B)
Int A is Element of K10( the carrier of B)
(Cl A) \ (Int A) is Element of K10( the carrier of B)
A ` is Element of K10( the carrier of B)
the carrier of B \ A is set
Cl (A `) is Element of K10( the carrier of B)
(Cl (A `)) ` is Element of K10( the carrier of B)
the carrier of B \ (Cl (A `)) is set
((Cl (A `)) `) ` is Element of K10( the carrier of B)
the carrier of B \ ((Cl (A `)) `) is set
(Cl A) /\ (((Cl (A `)) `) `) is Element of K10( the carrier of B)
(Cl A) \ ((Cl (A `)) `) is Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
Fr A is closed Element of K10( the carrier of B)
B is Element of the carrier of B
A is Element of K10( the carrier of B)
A ` is Element of K10( the carrier of B)
the carrier of B \ A is set
A \ A is Element of K10( the carrier of B)
A is Element of K10( the carrier of B)
A \ A is Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10( the carrier of B)
Fr A is closed Element of K10( the carrier of B)
B is Element of the carrier of B
c<sub>5</sub> is Element of K10( the carrier of B)
A is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
c<sub>5</sub> \ A is Element of K10( the carrier of B)
A ` is Element of K10( the carrier of B)
the carrier of B \ A is set
the V115(B,B) V129(B) Element of K10(K10( the carrier of B)) is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
c₅ is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
B \ A is Element of K10( the carrier of B)
c₅ \ A is Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10( the carrier of B)
Fr A is closed Element of K10( the carrier of B)
B is Element of the carrier of B
the V115(B,B) V129(B) Element of K10(K10( the carrier of B)) is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
B is Element of K10( the carrier of B)
c₅ is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
B \ A is Element of K10( the carrier of B)
A is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
A ` is Element of K10( the carrier of B)
the carrier of B \ A is set
c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
B \ A is Element of K10( the carrier of B)
c<sub>5</sub> \ A is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
A /\ B is Element of K10( the carrier of B)
Fr (A /\ B) is closed Element of K10( the carrier of B)
Cl A is closed Element of K10( the carrier of B)
Fr B is closed Element of K10( the carrier of B)
(Cl A) /\ (Fr B) is closed Element of K10( the carrier of B)
Fr A is closed Element of K10( the carrier of B)
Cl B is closed Element of K10( the carrier of B)
(Fr A) /\ (Cl B) is closed Element of K10( the carrier of B)
((Cl A) /\ (Fr B)) \/ ((Fr A) /\ (Cl B)) is closed Element of K10( the carrier of B)
(Cl A) /\ (Cl B) is closed Element of K10( the carrier of B)
A ` is Element of K10( the carrier of B)
the carrier of B \ A is set
Cl (A `) is closed Element of K10( the carrier of B)
B ` is Element of K10( the carrier of B)
the carrier of B \ B is set
Cl (B `) is closed Element of K10( the carrier of B)
(Cl (A `)) \/ (Cl (B `)) is closed Element of K10( the carrier of B)
((Cl A) /\ (Cl B)) /\ ((Cl (A `)) \/ (Cl (B `))) is closed Element of K10( the carrier of B)
((Cl A) /\ (Cl B)) /\ (Cl (A `)) is closed Element of K10( the carrier of B)
((Cl A) /\ (Cl B)) /\ (Cl (B `)) is closed Element of K10( the carrier of B)
(((Cl A) /\ (Cl B)) /\ (Cl (A `))) \/ (((Cl A) /\ (Cl B)) /\ (Cl (B `))) is closed Element of K10( the carrier of B)
(Cl A) /\ (Cl (A `)) is closed Element of K10( the carrier of B)
((Cl A) /\ (Cl (A `))) /\ (Cl B) is closed Element of K10( the carrier of B)
(((Cl A) /\ (Cl (A `))) /\ (Cl B)) \/ (((Cl A) /\ (Cl B)) /\ (Cl (B `))) is closed Element of K10( the carrier of B)
((Fr A) /\ (Cl B)) \/ (((Cl A) /\ (Cl B)) /\ (Cl (B `))) is closed Element of K10( the carrier of B)
(Cl B) /\ (Cl (B `)) is closed Element of K10( the carrier of B)
(Cl A) /\ ((Cl B) /\ (Cl (B `))) is closed Element of K10( the carrier of B)
((Fr A) /\ (Cl B)) \/ ((Cl A) /\ ((Cl B) /\ (Cl (B `)))) is closed Element of K10( the carrier of B)
((Fr A) /\ (Cl B)) \/ ((Cl A) /\ (Fr B)) is closed Element of K10( the carrier of B)
Cl (A /\ B) is closed Element of K10( the carrier of B)
(A /\ B) ` is Element of K10( the carrier of B)
the carrier of B \ (A /\ B) is set
Cl ((A /\ B) `) is closed Element of K10( the carrier of B)
(Cl (A /\ B)) /\ (Cl ((A /\ B) `)) is closed Element of K10( the carrier of B)
(A `) \/ (B `) is Element of K10( the carrier of B)
Cl ((A `) \/ (B `)) is closed Element of K10( the carrier of B)
(Cl (A /\ B)) /\ (Cl ((A `) \/ (B `))) is closed Element of K10( the carrier of B)
(Cl (A /\ B)) /\ ((Cl (A `)) \/ (Cl (B `))) is closed Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
Int A is open Element of K10( the carrier of B)
Fr A is closed Element of K10( the carrier of B)
(Int A) \/ (Fr A) is Element of K10( the carrier of B)
A ` is Element of K10( the carrier of B)
the carrier of B \ A is set
Int (A `) is open Element of K10( the carrier of B)
((Int A) \/ (Fr A)) \/ (Int (A `)) is Element of K10( the carrier of B)
(Int A) \/ (Int (A `)) is open Element of K10( the carrier of B)
((Int A) \/ (Int (A `))) \/ (Fr A) is Element of K10( the carrier of B)
Cl A is closed Element of K10( the carrier of B)
Cl (A `) is closed Element of K10( the carrier of B)
(Cl A) /\ (Cl (A `)) is closed Element of K10( the carrier of B)
((Int A) \/ (Int (A `))) \/ ((Cl A) /\ (Cl (A `))) is Element of K10( the carrier of B)
((Int A) \/ (Int (A `))) \/ (Cl A) is Element of K10( the carrier of B)
((Int A) \/ (Int (A `))) \/ (Cl (A `)) is Element of K10( the carrier of B)
(((Int A) \/ (Int (A `))) \/ (Cl A)) /\ (((Int A) \/ (Int (A `))) \/ (Cl (A `))) is Element of K10( the carrier of B)
(Cl A) ` is open Element of K10( the carrier of B)
the carrier of B \ (Cl A) is set
(Int A) \/ ((Cl A) `) is open Element of K10( the carrier of B)
((Int A) \/ ((Cl A) `)) \/ (Cl A) is Element of K10( the carrier of B)
(((Int A) \/ ((Cl A) `)) \/ (Cl A)) /\ (((Int A) \/ (Int (A `))) \/ (Cl (A `))) is Element of K10( the carrier of B)
((Cl A) `) \/ (Cl A) is Element of K10( the carrier of B)
(Int A) \/ (((Cl A) `) \/ (Cl A)) is Element of K10( the carrier of B)
((Int A) \/ (((Cl A) `) \/ (Cl A))) /\ (((Int A) \/ (Int (A `))) \/ (Cl (A `))) is Element of K10( the carrier of B)
[#] B is non proper open dense Element of K10( the carrier of B)
(Int A) \/ ([#] B) is open Element of K10( the carrier of B)
((Int A) \/ ([#] B)) /\ (((Int A) \/ (Int (A `))) \/ (Cl (A `))) is Element of K10( the carrier of B)
(Int A) ` is closed Element of K10( the carrier of B)
the carrier of B \ (Int A) is set
((Int A) \/ (Int (A `))) \/ ((Int A) `) is Element of K10( the carrier of B)
((Int A) \/ ([#] B)) /\ (((Int A) \/ (Int (A `))) \/ ((Int A) `)) is Element of K10( the carrier of B)
(Int A) \/ ((Int A) `) is Element of K10( the carrier of B)
((Int A) \/ ((Int A) `)) \/ (Int (A `)) is Element of K10( the carrier of B)
((Int A) \/ ([#] B)) /\ (((Int A) \/ ((Int A) `)) \/ (Int (A `))) is Element of K10( the carrier of B)
([#] B) \/ (Int (A `)) is open Element of K10( the carrier of B)
((Int A) \/ ([#] B)) /\ (([#] B) \/ (Int (A `))) is open Element of K10( the carrier of B)
([#] B) /\ (([#] B) \/ (Int (A `))) is open Element of K10( the carrier of B)
([#] B) /\ ([#] B) is open Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
Fr A is closed Element of K10( the carrier of B)
Int A is open Element of K10( the carrier of B)
A \ (Int A) is Element of K10( the carrier of B)
Cl A is closed Element of K10( the carrier of B)
(Cl A) \ (Int A) is Element of K10( the carrier of B)
B is TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is set
{B} is non empty V2() 1 -element set
A \ {B} is Element of K10( the carrier of B)
Cl (A \ {B}) is closed Element of K10( the carrier of B)
B is TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
A is set
B is Element of K10( the carrier of B)
A is Element of K10( the carrier of B)
c<sub>5</sub> is set
c<sub>5</sub> is set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
B is set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
B is Element of the carrier of B
{B} is non empty V2() 1 -element Element of K10( the carrier of B)
A \ {B} is Element of K10( the carrier of B)
Cl (A \ {B}) is closed Element of K10( the carrier of B)
A is open Element of K10( the carrier of B)
c<sub>5</sub> is set
B is Element of the carrier of B
q is Element of the carrier of B
A /\ A is Element of K10( the carrier of B)
A is Element of K10( the carrier of B)
A /\ A is Element of K10( the carrier of B)
c<sub>5</sub> is Element of the carrier of B
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
B is Element of the carrier of B
{B} is non empty V2() 1 -element Element of K10( the carrier of B)
A \ {B} is Element of K10( the carrier of B)
Cl (A \ {B}) is closed Element of K10( the carrier of B)
c<sub>5</sub> is Element of K10( the carrier of B)
A is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
B is set
q is Element of the carrier of B
q is Element of the carrier of B
A /\ c<sub>5</sub> is Element of K10( the carrier of B)
the V115(B,B) V129(B) Element of K10(K10( the carrier of B)) is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
A /\ B is Element of K10( the carrier of B)
A /\ c<sub>5</sub> is Element of K10( the carrier of B)
q is Element of the carrier of B
q is Element of the carrier of B
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
B is Element of the carrier of B
the V115(B,B) V129(B) Element of K10(K10( the carrier of B)) is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
{B} is non empty V2() 1 -element Element of K10( the carrier of B)
A \ {B} is Element of K10( the carrier of B)
Cl (A \ {B}) is closed Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
c<sub>5</sub> is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
q is set
q is Element of the carrier of B
U is Element of the carrier of B
A /\ B is Element of K10( the carrier of B)
A is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
A /\ B is Element of K10( the carrier of B)
A /\ c<sub>5</sub> is Element of K10( the carrier of B)
q is Element of the carrier of B
q is Element of the carrier of B
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
A \ (B,A) is Element of K10( the carrier of B)
B is set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is Element of the carrier of B
(B,A) is Element of K10( the carrier of B)
A is open Element of K10( the carrier of B)
A /\ A is Element of K10( the carrier of B)
c<sub>5</sub> is Element of the carrier of B
B is Element of the carrier of B
A is open Element of K10( the carrier of B)
A /\ A is Element of K10( the carrier of B)
c<sub>5</sub> is Element of the carrier of B
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is Element of the carrier of B
{B} is non empty V2() 1 -element Element of K10( the carrier of B)
A is open Element of K10( the carrier of B)
c<sub>5</sub> is open Element of K10( the carrier of B)
c<sub>5</sub> /\ A is Element of K10( the carrier of B)
B is set
B is set
A is open Element of K10( the carrier of B)
A /\ A is Element of K10( the carrier of B)
c<sub>5</sub> is Element of the carrier of B
A /\ A is Element of K10( the carrier of B)
c<sub>5</sub> is Element of the carrier of B
c<sub>5</sub> is open Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
A is Element of the carrier of B
{A} is non empty V2() 1 -element Element of K10( the carrier of B)
K10( the carrier of B) is non empty set
[#] B is non empty non proper open dense non boundary Element of K10( the carrier of B)
{A} /\ ([#] B) is Element of K10( the carrier of B)
B is open Element of K10( the carrier of B)
B /\ ([#] B) is open Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
B is Element of K10(K10( the carrier of B))
A is Element of K10(K10( the carrier of B))
c<sub>5</sub> is set
B is Element of K10( the carrier of B)
q is Element of K10( the carrier of B)
(B,q) is Element of K10( the carrier of B)
c<sub>5</sub> is set
B is Element of K10( the carrier of B)
(B,B) is Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
(B,A) is Element of K10(K10( the carrier of B))
B is set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10( the carrier of B)
{A} is non empty V2() 1 -element Element of K10(K10( the carrier of B))
(B,A) is Element of K10( the carrier of B)
{(B,A)} is non empty V2() 1 -element Element of K10(K10( the carrier of B))
B is Element of K10(K10( the carrier of B))
(B,B) is Element of K10(K10( the carrier of B))
A is set
c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
(B,B) is Element of K10( the carrier of B)
A is set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
(B,A) is Element of K10(K10( the carrier of B))
B is Element of K10(K10( the carrier of B))
(B,B) is Element of K10(K10( the carrier of B))
A is set
c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
(B,B) is Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
(B,A) is Element of K10(K10( the carrier of B))
B is Element of K10(K10( the carrier of B))
A \/ B is Element of K10(K10( the carrier of B))
(B,(A \/ B)) is Element of K10(K10( the carrier of B))
(B,B) is Element of K10(K10( the carrier of B))
(B,A) \/ (B,B) is Element of K10(K10( the carrier of B))
A is set
c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
(B,B) is Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
Cl A is closed Element of K10( the carrier of B)
B is set
A is Element of the carrier of B
c<sub>5</sub> is Element of K10( the carrier of B)
A /\ c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of the carrier of B
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
Cl A is closed Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
A \/ (B,A) is Element of K10( the carrier of B)
B is set
A is Element of the carrier of B
c<sub>5</sub> is open Element of K10( the carrier of B)
A /\ c<sub>5</sub> is Element of K10( the carrier of B)
B is set
q is Element of the carrier of B
B is set
{} \/ {} is set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
(B,B) is Element of K10( the carrier of B)
A is set
c<sub>5</sub> is Element of the carrier of B
B is open Element of K10( the carrier of B)
B /\ B is Element of K10( the carrier of B)
A /\ B is Element of K10( the carrier of B)
q is Element of the carrier of B
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
A \/ B is Element of K10( the carrier of B)
(B,(A \/ B)) is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
(B,B) is Element of K10( the carrier of B)
(B,A) \/ (B,B) is Element of K10( the carrier of B)
A is set
{A} is non empty V2() 1 -element set
(A \/ B) \ {A} is Element of K10( the carrier of B)
Cl ((A \/ B) \ {A}) is closed Element of K10( the carrier of B)
A \ {A} is Element of K10( the carrier of B)
B \ {A} is Element of K10( the carrier of B)
(A \ {A}) \/ (B \ {A}) is Element of K10( the carrier of B)
Cl (A \ {A}) is closed Element of K10( the carrier of B)
Cl (B \ {A}) is closed Element of K10( the carrier of B)
(Cl (A \ {A})) \/ (Cl (B \ {A})) is closed Element of K10( the carrier of B)
A is set
{A} is non empty V2() 1 -element set
(A \/ B) \ {A} is Element of K10( the carrier of B)
Cl ((A \/ B) \ {A}) is closed Element of K10( the carrier of B)
B \ {A} is Element of K10( the carrier of B)
Cl (B \ {A}) is closed Element of K10( the carrier of B)
A \ {A} is Element of K10( the carrier of B)
Cl (A \ {A}) is closed Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
(B,(B,A)) is Element of K10( the carrier of B)
B is set
A is Element of the carrier of B
c<sub>5</sub> is open Element of K10( the carrier of B)
A /\ c<sub>5</sub> is Element of K10( the carrier of B)
{A} is non empty V2() 1 -element Element of K10( the carrier of B)
Cl {A} is non empty closed Element of K10( the carrier of B)
c<sub>5</sub> \ {A} is Element of K10( the carrier of B)
(B,A) /\ c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of the carrier of B
{B} is non empty V2() 1 -element set
(B,A) \ {B} is Element of K10( the carrier of B)
q is set
q is Element of the carrier of B
c<sub>5</sub> \ {B} is Element of K10( the carrier of B)
A \ {B} is Element of K10( the carrier of B)
y is set
A /\ (c<sub>5</sub> \ {A}) is Element of K10( the carrier of B)
y is Element of the carrier of B
{q} is non empty V2() 1 -element Element of K10( the carrier of B)
A \ {q} is Element of K10( the carrier of B)
f is set
A \ {A} is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
Cl (B,A) is closed Element of K10( the carrier of B)
(B,(B,A)) is Element of K10( the carrier of B)
(B,A) \/ (B,(B,A)) is Element of K10( the carrier of B)
(B,A) \/ (B,A) is Element of K10( the carrier of B)
B is non empty TopSpace-like T_1 TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
Cl (B,A) is closed Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
(B,A) is Element of K10(K10( the carrier of B))
union (B,A) is Element of K10( the carrier of B)
union A is Element of K10( the carrier of B)
(B,(union A)) is Element of K10( the carrier of B)
B is set
A is set
c<sub>5</sub> is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
(B,B) is Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
A is set
(B,A) is Element of K10( the carrier of B)
(B,B) is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
Cl A is closed Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
A \/ (B,A) is Element of K10( the carrier of B)
(B,(Cl A)) is Element of K10( the carrier of B)
(B,(A \/ (B,A))) is Element of K10( the carrier of B)
(B,(B,A)) is Element of K10( the carrier of B)
(B,A) \/ (B,(B,A)) is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
union A is Element of K10( the carrier of B)
(B,A) is Element of K10(K10( the carrier of B))
union (B,A) is Element of K10( the carrier of B)
B is set
A is set
c<sub>5</sub> is Element of K10( the carrier of B)
(B,c<sub>5</sub>) is Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
union A is Element of K10( the carrier of B)
(B,A) is Element of K10(K10( the carrier of B))
union (B,A) is Element of K10( the carrier of B)
(B,(union A)) is Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
{} B is empty proper ordinal cardinal {} -element open boundary nowhere_dense Element of K10( the carrier of B)
the carrier of B is non empty set
K10( the carrier of B) is non empty set
Fr ({} B) is closed boundary nowhere_dense Element of K10( the carrier of B)
Cl ({} B) is empty proper ordinal cardinal {} -element open closed boundary nowhere_dense Element of K10( the carrier of B)
({} B) ` is closed dense Element of K10( the carrier of B)
the carrier of B \ ({} B) is set
Cl (({} B) `) is closed Element of K10( the carrier of B)
(Cl ({} B)) /\ (Cl (({} B) `)) is closed Element of K10( the carrier of B)
{} /\ (Cl (({} B) `)) is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is open closed Element of K10( the carrier of B)
Fr A is closed boundary nowhere_dense Element of K10( the carrier of B)
B is non empty V47() TopSpace-like non discrete TopStruct
the carrier of B is non empty V2() set
K10( the carrier of B) is non empty set
B is non empty V47() TopSpace-like non discrete TopStruct
the carrier of B is non empty V2() set
K10( the carrier of B) is non empty set
A is non open Element of K10( the carrier of B)
Fr A is closed Element of K10( the carrier of B)
B is non empty V47() TopSpace-like non discrete TopStruct
the carrier of B is non empty V2() set
K10( the carrier of B) is non empty set
A is non closed Element of K10( the carrier of B)
Fr A is closed Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
A is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
{} B is empty ordinal cardinal {} -element open boundary nowhere_dense Element of K10( the carrier of B)
the carrier of B is set
K10( the carrier of B) is non empty set
(B,({} B)) is Element of K10( the carrier of B)
Cl ({} B) is empty ordinal cardinal {} -element open closed boundary nowhere_dense Element of K10( the carrier of B)
({} B) \/ (B,({} B)) is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
Cl A is closed Element of K10( the carrier of B)
(B,A) \/ A is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
(B,A) is Element of K10( the carrier of B)
Cl A is closed Element of K10( the carrier of B)
(B,A) \/ A is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
{} B is empty ordinal cardinal {} -element open boundary nowhere_dense Element of K10( the carrier of B)
the carrier of B is set
K10( the carrier of B) is non empty set
(B,({} B)) is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
{} B is empty ordinal cardinal {} -element open boundary nowhere_dense Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
{} B is empty ordinal cardinal {} -element open closed boundary nowhere_dense (B) (B) Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
A is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
{} B is empty ordinal cardinal {} -element open closed boundary nowhere_dense (B) (B) Element of K10( the carrier of B)
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
{} B is empty ordinal cardinal {} -element open closed boundary nowhere_dense (B) (B) Element of K10( the carrier of B)
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
[#] B is non empty non proper open dense non boundary Element of K10( the carrier of B)
K10(K10( the carrier of B)) is non empty set
A is Element of K10(K10( the carrier of B))
union A is Element of K10( the carrier of B)
(union A) ` is Element of K10( the carrier of B)
the carrier of B \ (union A) is set
(union A) \/ ((union A) `) is Element of K10( the carrier of B)
Cl (union A) is closed Element of K10( the carrier of B)
A is Element of K10( the carrier of B)
B is TopSpace-like discrete TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
Fr A is closed Element of K10( the carrier of B)
B is TopSpace-like discrete TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)
B is Element of K10( the carrier of B)
B is TopSpace-like discrete TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
A is open closed Element of K10( the carrier of B)
(B,A) is open closed Element of K10( the carrier of B)
B is set
{B} is non empty V2() 1 -element set
A \ {B} is open closed Element of K10( the carrier of B)
Cl (A \ {B}) is open closed Element of K10( the carrier of B)
B is non empty TopSpace-like T_1 T_2 V64() normal discrete TopStruct
the carrier of B is non empty set
K10( the carrier of B) is non empty set
A is open closed Element of K10( the carrier of B)
(B,A) is open closed Element of K10( the carrier of B)
B is TopSpace-like TopStruct
the carrier of B is set
K10( the carrier of B) is non empty set
[#] B is non proper open dense Element of K10( the carrier of B)
card ([#] B) is ordinal cardinal set
B is ordinal set
A is Element of K10( the carrier of B)
card A is ordinal cardinal set
A is Element of K10( the carrier of B)
card A is ordinal cardinal set
c<sub>5</sub> is Element of K10( the carrier of B)
card c<sub>5</sub> is ordinal cardinal set
A is ordinal cardinal set
B is ordinal cardinal set
A is Element of K10( the carrier of B)
card A is ordinal cardinal set
c<sub>5</sub> is Element of K10( the carrier of B)
card c<sub>5</sub> is ordinal cardinal set
B is TopSpace-like countable TopStruct
[#] B is non proper countable open dense Element of K10( the carrier of B)
the carrier of B is set
K10( the carrier of B) is non empty set
card ([#] B) is ordinal cardinal set
(B) is ordinal cardinal set
B is TopSpace-like TopStruct
B is Element of K10( the carrier of R^1)
B ` is Element of K10( the carrier of R^1)
the carrier of R^1 \ B is set
REAL \ IRRAT is Element of K10(REAL)
REAL /\ RAT is set
B is Element of K10( the carrier of R^1)
B ` is Element of K10( the carrier of R^1)
the carrier of R^1 \ B is set
B is Element of K10( the carrier of R^1)
Int B is open Element of K10( the carrier of R^1)
B ` is Element of K10( the carrier of R^1)
the carrier of R^1 \ B is set
Cl (B `) is closed Element of K10( the carrier of R^1)
[#] R^1 is non empty non proper open dense non boundary Element of K10( the carrier of R^1)
(Cl (B `)) ` is open Element of K10( the carrier of R^1)
the carrier of R^1 \ (Cl (B `)) is set
{} R^1 is empty proper ordinal cardinal {} -element open closed boundary nowhere_dense ( R^1 ) ( R^1 ) ( R^1 ) Element of K10( the carrier of R^1)
B is Element of K10( the carrier of R^1)
Int B is open Element of K10( the carrier of R^1)
B ` is Element of K10( the carrier of R^1)
the carrier of R^1 \ B is set
Cl (B `) is closed Element of K10( the carrier of R^1)
[#] R^1 is non empty non proper open dense non boundary Element of K10( the carrier of R^1)
(Cl (B `)) ` is open Element of K10( the carrier of R^1)
the carrier of R^1 \ (Cl (B `)) is set
{} R^1 is empty proper ordinal cardinal {} -element open closed boundary nowhere_dense ( R^1 ) ( R^1 ) ( R^1 ) Element of K10( the carrier of R^1)
B is Element of K10( the carrier of R^1)
Cl B is closed Element of K10( the carrier of R^1)
A is Element of K10( the carrier of R^1)
Cl A is closed Element of K10( the carrier of R^1)
B is Element of K10( the carrier of R^1)
B ` is Element of K10( the carrier of R^1)
the carrier of R^1 \ B is set
A is Element of K10( the carrier of R^1)
A ` is Element of K10( the carrier of R^1)
the carrier of R^1 \ A is set
[#] REAL is non proper Element of K10(REAL)
[#] R^1 is non empty non proper open dense non boundary Element of K10( the carrier of R^1)
A is Element of K10( the carrier of R^1)
B is Element of K10( the carrier of R^1)
A \/ B is Element of K10( the carrier of R^1)
RAT \/ REAL is set