:: TOPGEN_1 semantic presentation

K10(omega) is non empty non finite set
REAL is set
K10(REAL) is non empty set

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

[#] 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

[#] 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 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

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))
c5 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)
c5 is set
B is Element of K10( the carrier of B)
Fr B is closed Element of K10( the carrier of B)

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)

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

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
c5 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)

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
c5 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
c5 is Element of K10( the carrier of B)
A is V115(B,B) V129(B) Element of K10(K10( the carrier of B))
c5 \ 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))
c5 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)
c5 \ 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)
c5 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
c5 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)
c5 \ A is 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 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)

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)

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

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)
c5 is set
c5 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)
c5 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)
c5 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)
c5 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 /\ c5 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))
c5 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 /\ c5 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)
c5 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))
c5 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 /\ c5 is Element of K10( the carrier of B)
q is Element of the carrier of B
q is Element of the carrier of B

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)
c5 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)
c5 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)
c5 is open Element of K10( the carrier of B)
c5 /\ 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)
c5 is Element of the carrier of B
A /\ A is Element of K10( the carrier of B)
c5 is Element of the carrier of B
c5 is open Element of K10( the carrier of B)

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)

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))
c5 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)
c5 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
c5 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
c5 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
c5 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
c5 is Element of K10( the carrier of B)
A /\ c5 is Element of K10( the carrier of B)
B is Element of 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)
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
c5 is open Element of K10( the carrier of B)
A /\ c5 is Element of K10( the carrier of B)
B is set
q is Element of 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 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
c5 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
c5 is open Element of K10( the carrier of B)
A /\ c5 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)
c5 \ {A} is Element of K10( the carrier of B)
(B,A) /\ c5 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
c5 \ {B} is Element of K10( the carrier of B)
A \ {B} is Element of K10( the carrier of B)
y is set
A /\ (c5 \ {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)

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,()) is Element of K10( the carrier of B)
B is set
A is set
c5 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)

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)

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
c5 is Element of K10( the carrier of B)
(B,c5) 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,()) 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
Fr ({} B) is 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)

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)

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

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)

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) \/ (B,({} B)) is 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,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)

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)

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)

the carrier of B is set
K10( the carrier of B) is non empty set
A is Element of K10( the carrier of B)

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)

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

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)
() ` is Element of K10( the carrier of B)
the carrier of B \ () is set
() \/ (() `) is Element of K10( the carrier of B)
Cl () is closed Element of K10( the carrier of B)
A is 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)
Fr A is closed 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 Element of K10( the carrier of B)

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)

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)

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)

B is ordinal set
A is Element of K10( the carrier of B)

A is Element of K10( the carrier of B)

c5 is Element of K10( the carrier of B)

A is Element of K10( the carrier of B)

c5 is Element of K10( the carrier of B)

[#] 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

(B) is ordinal cardinal 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
REAL \ IRRAT is Element of K10(REAL)

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

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

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)