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

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

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

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

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

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

A is V115(B,B) V129(B) Element of K10(K10( the carrier of B))

c

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

B is Element of K10( the carrier of B)

B \ A is Element of K10( the carrier of B)

c

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

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

B is Element of K10( the carrier of B)

B \ A is Element of K10( the carrier of B)

c

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

c

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

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

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

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

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

B is Element of K10( the carrier of B)

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

A /\ c

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

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

B is Element of K10( the carrier of B)

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

A /\ c

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

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

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

c

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

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

c

c

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

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

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

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

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

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

A /\ c

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

A /\ c

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

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

A /\ c

{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

(B,A) /\ c

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

A \ {B} is Element of K10( the carrier of B)

y is set

A /\ (c

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

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

(B,c

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

card c

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

card c

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