:: TOPS_1 semantic presentation

K96() is set

K10(K96()) is non empty set

{} is empty set

the empty set is empty set

1 is non empty set

GX is 1-sorted

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

x is Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

GX is TopStruct

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

the carrier of GX is set

K10( the carrier of GX) is non empty set

Cl ([#] GX) is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

Cl (Cl R) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

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

([#] GX) \ R is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

(R `) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R `) is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

{} GX is empty closed Element of K10( the carrier of GX)

({} GX) ` is open Element of K10( the carrier of GX)

the carrier of GX \ ({} GX) is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is open Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

Cl x is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

(Cl R) \ (Cl x) is Element of K10( the carrier of GX)

R \ x is Element of K10( the carrier of GX)

Cl (R \ x) is closed Element of K10( the carrier of GX)

x99 is set

(Cl R) \/ (Cl x) is Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

Cl (R \/ x) is closed Element of K10( the carrier of GX)

(R \ x) \/ x is Element of K10( the carrier of GX)

Cl ((R \ x) \/ x) is closed Element of K10( the carrier of GX)

(Cl (R \ x)) \/ (Cl x) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

Cl (R /\ x) is Element of K10( the carrier of GX)

Cl x is Element of K10( the carrier of GX)

(Cl R) /\ (Cl x) is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is closed Element of K10( the carrier of GX)

x is closed Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

Cl (R /\ x) is closed Element of K10( the carrier of GX)

x99 is Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

Cl (R \/ x) is closed Element of K10( the carrier of GX)

x99 is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is open Element of K10( the carrier of GX)

x is open Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

R ` is closed Element of K10( the carrier of GX)

the carrier of GX \ R is set

x ` is closed Element of K10( the carrier of GX)

the carrier of GX \ x is set

(R `) \/ (x `) is closed Element of K10( the carrier of GX)

(R /\ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R /\ x) is set

x99 is Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

R ` is closed Element of K10( the carrier of GX)

the carrier of GX \ R is set

x ` is closed Element of K10( the carrier of GX)

the carrier of GX \ x is set

(R `) /\ (x `) is closed Element of K10( the carrier of GX)

(R \/ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R \/ x) is set

x99 is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

GX is non empty TopSpace-like TopStruct

the carrier of GX is non empty set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

x is Element of the carrier of GX

x99 is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

x99 ` is Element of K10( the carrier of GX)

the carrier of GX \ x99 is set

(R `) \/ (x99 `) is Element of K10( the carrier of GX)

R /\ x99 is Element of K10( the carrier of GX)

(R /\ x99) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R /\ x99) is set

{} GX is empty proper closed Element of K10( the carrier of GX)

Q1 is set

Cl (x99 `) is closed Element of K10( the carrier of GX)

(Cl R) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl R) is set

R /\ (R `) is Element of K10( the carrier of GX)

R /\ ((Cl R) `) is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

R /\ (Cl x) is Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

Cl (R /\ x) is closed Element of K10( the carrier of GX)

x99 is set

Q1 is Element of the carrier of GX

Q1 is Element of K10( the carrier of GX)

Q1 /\ R is Element of K10( the carrier of GX)

x /\ (Q1 /\ R) is Element of K10( the carrier of GX)

(R /\ x) /\ Q1 is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

R /\ (Cl x) is Element of K10( the carrier of GX)

Cl (R /\ (Cl x)) is closed Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

Cl (R /\ x) is closed Element of K10( the carrier of GX)

x99 is set

Q1 is Element of the carrier of GX

Q1 is Element of K10( the carrier of GX)

(R /\ x) /\ Q1 is Element of K10( the carrier of GX)

(R /\ (Cl x)) /\ Q1 is Element of K10( the carrier of GX)

Cl (Cl (R /\ x)) is closed Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

x is Element of K10( the carrier of GX)

x99 is Element of K10( the carrier of GX)

x99 ` is Element of K10( the carrier of GX)

the carrier of GX \ x99 is set

Cl (x99 `) is Element of K10( the carrier of GX)

(Cl (x99 `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (x99 `)) is set

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is Element of K10( the carrier of GX)

(Cl (x `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (x `)) is set

GX is TopSpace-like TopStruct

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

the carrier of GX is set

K10( the carrier of GX) is non empty set

(GX,([#] GX)) is Element of K10( the carrier of GX)

([#] GX) ` is open Element of K10( the carrier of GX)

the carrier of GX \ ([#] GX) is set

Cl (([#] GX) `) is closed Element of K10( the carrier of GX)

(Cl (([#] GX) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (([#] GX) `)) is set

{} GX is empty closed Element of K10( the carrier of GX)

({} GX) ` is open Element of K10( the carrier of GX)

the carrier of GX \ ({} GX) is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

x is set

x99 is Element of the carrier of GX

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl (R `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

x is Element of K10( the carrier of GX)

(GX,x) is Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is closed Element of K10( the carrier of GX)

(Cl (x `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (x `)) is set

(GX,R) /\ (GX,x) is Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

(GX,(R /\ x)) is Element of K10( the carrier of GX)

(R /\ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R /\ x) is set

Cl ((R /\ x) `) is closed Element of K10( the carrier of GX)

(Cl ((R /\ x) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((R /\ x) `)) is set

(Cl (R `)) \/ (Cl (x `)) is closed Element of K10( the carrier of GX)

((Cl (R `)) \/ (Cl (x `))) ` is open Element of K10( the carrier of GX)

the carrier of GX \ ((Cl (R `)) \/ (Cl (x `))) is set

(R `) \/ (x `) is Element of K10( the carrier of GX)

Cl ((R `) \/ (x `)) is closed Element of K10( the carrier of GX)

(Cl ((R `) \/ (x `))) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((R `) \/ (x `))) is set

GX is TopStruct

{} GX is empty Element of K10( the carrier of GX)

the carrier of GX is set

K10( the carrier of GX) is non empty set

(GX,({} GX)) is Element of K10( the carrier of GX)

({} GX) ` is Element of K10( the carrier of GX)

the carrier of GX \ ({} GX) is set

Cl (({} GX) `) is Element of K10( the carrier of GX)

(Cl (({} GX) `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (({} GX) `)) is set

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

([#] GX) ` is Element of K10( the carrier of GX)

the carrier of GX \ ([#] GX) is set

GX is TopStruct

{} GX is empty Element of K10( the carrier of GX)

the carrier of GX is set

K10( the carrier of GX) is non empty set

(GX,({} GX)) is empty Element of K10( the carrier of GX)

({} GX) ` is Element of K10( the carrier of GX)

the carrier of GX \ ({} GX) is set

Cl (({} GX) `) is Element of K10( the carrier of GX)

(Cl (({} GX) `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (({} GX) `)) is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

x is Element of K10( the carrier of GX)

(GX,x) is Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is Element of K10( the carrier of GX)

(Cl (x `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (x `)) is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

x is Element of K10( the carrier of GX)

(GX,x) is Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is Element of K10( the carrier of GX)

(Cl (x `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (x `)) is set

(GX,R) \/ (GX,x) is Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

(GX,(R \/ x)) is Element of K10( the carrier of GX)

(R \/ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R \/ x) is set

Cl ((R \/ x) `) is Element of K10( the carrier of GX)

(Cl ((R \/ x) `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((R \/ x) `)) is set

(R `) /\ (x `) is Element of K10( the carrier of GX)

Cl ((R `) /\ (x `)) is Element of K10( the carrier of GX)

(Cl (R `)) /\ (Cl (x `)) is Element of K10( the carrier of GX)

((Cl (R `)) /\ (Cl (x `))) ` is Element of K10( the carrier of GX)

the carrier of GX \ ((Cl (R `)) /\ (Cl (x `))) is set

(Cl ((R `) /\ (x `))) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((R `) /\ (x `))) is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl (R `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

x is Element of K10( the carrier of GX)

R \ x is Element of K10( the carrier of GX)

(GX,(R \ x)) is Element of K10( the carrier of GX)

(R \ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R \ x) is set

Cl ((R \ x) `) is closed Element of K10( the carrier of GX)

(Cl ((R \ x) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((R \ x) `)) is set

(GX,x) is Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is closed Element of K10( the carrier of GX)

(Cl (x `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (x `)) is set

(GX,R) \ (GX,x) is Element of K10( the carrier of GX)

R /\ (x `) is Element of K10( the carrier of GX)

(R /\ (x `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R /\ (x `)) is set

Cl ((R /\ (x `)) `) is closed Element of K10( the carrier of GX)

(Cl ((R /\ (x `)) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((R /\ (x `)) `)) is set

(x `) ` is Element of K10( the carrier of GX)

the carrier of GX \ (x `) is set

(R `) \/ ((x `) `) is Element of K10( the carrier of GX)

Cl ((R `) \/ ((x `) `)) is closed Element of K10( the carrier of GX)

(Cl ((R `) \/ ((x `) `))) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((R `) \/ ((x `) `))) is set

Cl x is closed Element of K10( the carrier of GX)

(Cl (R `)) \/ (Cl x) is closed Element of K10( the carrier of GX)

((Cl (R `)) \/ (Cl x)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ ((Cl (R `)) \/ (Cl x)) is set

(Cl x) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl x) is set

((Cl x) `) /\ (GX,R) is Element of K10( the carrier of GX)

(GX,x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (GX,x) is set

(GX,R) /\ ((GX,x) `) is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl (R `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

{} GX is empty closed Element of K10( the carrier of GX)

(GX,({} GX)) is empty open closed Element of K10( the carrier of GX)

({} GX) ` is open Element of K10( the carrier of GX)

the carrier of GX \ ({} GX) is set

Cl (({} GX) `) is closed Element of K10( the carrier of GX)

(Cl (({} GX) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (({} GX) `)) is set

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

(GX,([#] GX)) is open Element of K10( the carrier of GX)

([#] GX) ` is open Element of K10( the carrier of GX)

the carrier of GX \ ([#] GX) is set

Cl (([#] GX) `) is closed Element of K10( the carrier of GX)

(Cl (([#] GX) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (([#] GX) `)) is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

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

GX is non empty TopSpace-like TopStruct

the carrier of GX is non empty set

K10( the carrier of GX) is non empty set

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

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is set

x is Element of K10( the carrier of GX)

(GX,x) is open Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is closed Element of K10( the carrier of GX)

(Cl (x `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (x `)) is set

x99 is Element of K10( the carrier of GX)

x99 ` is Element of K10( the carrier of GX)

the carrier of GX \ x99 is set

Cl (x99 `) is closed Element of K10( the carrier of GX)

(x99 `) ` is Element of K10( the carrier of GX)

the carrier of GX \ (x99 `) is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is TopStruct

the carrier of R is set

K10( the carrier of R) is non empty set

x is Element of K10( the carrier of GX)

(GX,x) is open Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is closed Element of K10( the carrier of GX)

(Cl (x `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (x `)) is set

x99 is Element of K10( the carrier of R)

(R,x99) is Element of K10( the carrier of R)

x99 ` is Element of K10( the carrier of R)

the carrier of R \ x99 is set

Cl (x99 `) is Element of K10( the carrier of R)

(Cl (x99 `)) ` is Element of K10( the carrier of R)

the carrier of R \ (Cl (x99 `)) is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

(GX,x) is Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is Element of K10( the carrier of GX)

(Cl (x `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (x `)) is set

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is set

Q1 is Element of K10( the carrier of GX)

x99 is set

x is set

x99 is Element of K10( the carrier of GX)

(GX,R) is open Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl (R `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

x99 is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

Cl (GX,R) is Element of K10( the carrier of GX)

(GX,(Cl (GX,R))) is Element of K10( the carrier of GX)

(Cl (GX,R)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (GX,R)) is set

Cl ((Cl (GX,R)) `) is Element of K10( the carrier of GX)

(Cl ((Cl (GX,R)) `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((Cl (GX,R)) `)) is set

Cl (GX,(Cl (GX,R))) is Element of K10( the carrier of GX)

(GX,(GX,R)) is Element of K10( the carrier of GX)

(GX,R) ` is Element of K10( the carrier of GX)

the carrier of GX \ (GX,R) is set

Cl ((GX,R) `) is Element of K10( the carrier of GX)

(Cl ((GX,R) `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((GX,R) `)) is set

Cl (Cl (GX,R)) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

(GX,(Cl R)) is Element of K10( the carrier of GX)

(Cl R) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl R) is set

Cl ((Cl R) `) is Element of K10( the carrier of GX)

(Cl ((Cl R) `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((Cl R) `)) is set

Cl (GX,(Cl R)) is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

Cl (GX,R) is Element of K10( the carrier of GX)

(GX,(Cl (GX,R))) is Element of K10( the carrier of GX)

(Cl (GX,R)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (GX,R)) is set

Cl ((Cl (GX,R)) `) is Element of K10( the carrier of GX)

(Cl ((Cl (GX,R)) `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((Cl (GX,R)) `)) is set

Cl (GX,(Cl (GX,R))) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

GX is non empty TopSpace-like TopStruct

the carrier of GX is non empty set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

x is Element of the carrier of GX

x99 is Element of K10( the carrier of GX)

x99 is Element of K10( the carrier of GX)

x99 is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

(GX,(R `)) is Element of K10( the carrier of GX)

(R `) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R `) is set

Cl ((R `) `) is Element of K10( the carrier of GX)

(Cl (R `)) /\ (Cl ((R `) `)) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

(Cl (R `)) /\ R is Element of K10( the carrier of GX)

(Cl R) \ R is Element of K10( the carrier of GX)

((Cl (R `)) /\ R) \/ ((Cl R) \ R) is Element of K10( the carrier of GX)

x is set

x99 is Element of the carrier of GX

x99 is Element of the carrier of GX

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

R \/ (GX,R) is Element of K10( the carrier of GX)

R \/ (Cl R) is Element of K10( the carrier of GX)

R \/ (Cl (R `)) is Element of K10( the carrier of GX)

(R \/ (Cl R)) /\ (R \/ (Cl (R `))) is Element of K10( the carrier of GX)

(Cl R) /\ (R \/ (Cl (R `))) is Element of K10( the carrier of GX)

(Cl R) \ R is Element of K10( the carrier of GX)

R \/ ((Cl R) \ R) is Element of K10( the carrier of GX)

R \/ ((Cl R) /\ (Cl (R `))) is Element of K10( the carrier of GX)

x is set

x99 is Element of the carrier of GX

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

(GX,(R /\ x)) is closed Element of K10( the carrier of GX)

Cl (R /\ x) is closed Element of K10( the carrier of GX)

(R /\ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R /\ x) is set

Cl ((R /\ x) `) is closed Element of K10( the carrier of GX)

(Cl (R /\ x)) /\ (Cl ((R /\ x) `)) is closed Element of K10( the carrier of GX)

(GX,x) is closed Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is closed Element of K10( the carrier of GX)

(Cl x) /\ (Cl (x `)) is closed Element of K10( the carrier of GX)

(GX,R) \/ (GX,x) is closed Element of K10( the carrier of GX)

(Cl (R /\ x)) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

(Cl (R /\ x)) /\ (Cl (x `)) is closed Element of K10( the carrier of GX)

(R `) \/ (x `) is Element of K10( the carrier of GX)

Cl ((R `) \/ (x `)) is closed Element of K10( the carrier of GX)

(Cl (R /\ x)) /\ (Cl ((R `) \/ (x `))) is closed Element of K10( the carrier of GX)

(Cl (R `)) \/ (Cl (x `)) is closed Element of K10( the carrier of GX)

(Cl (R /\ x)) /\ ((Cl (R `)) \/ (Cl (x `))) is closed Element of K10( the carrier of GX)

((Cl (R /\ x)) /\ (Cl (R `))) \/ ((Cl (R /\ x)) /\ (Cl (x `))) is closed Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

(GX,(R \/ x)) is closed Element of K10( the carrier of GX)

Cl (R \/ x) is closed Element of K10( the carrier of GX)

(R \/ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R \/ x) is set

Cl ((R \/ x) `) is closed Element of K10( the carrier of GX)

(Cl (R \/ x)) /\ (Cl ((R \/ x) `)) is closed Element of K10( the carrier of GX)

(GX,x) is closed Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is closed Element of K10( the carrier of GX)

(Cl x) /\ (Cl (x `)) is closed Element of K10( the carrier of GX)

(GX,R) \/ (GX,x) is closed Element of K10( the carrier of GX)

(R `) /\ (x `) is Element of K10( the carrier of GX)

Cl ((R `) /\ (x `)) is closed Element of K10( the carrier of GX)

(Cl ((R `) /\ (x `))) /\ (Cl R) is closed Element of K10( the carrier of GX)

(Cl (R `)) /\ (Cl R) is closed Element of K10( the carrier of GX)

(Cl ((R `) /\ (x `))) /\ (Cl x) is closed Element of K10( the carrier of GX)

(Cl (x `)) /\ (Cl x) is closed Element of K10( the carrier of GX)

(Cl R) \/ (Cl x) is closed Element of K10( the carrier of GX)

((Cl R) \/ (Cl x)) /\ (Cl ((R \/ x) `)) is closed Element of K10( the carrier of GX)

(Cl ((R `) /\ (x `))) /\ ((Cl R) \/ (Cl x)) is closed Element of K10( the carrier of GX)

((Cl ((R `) /\ (x `))) /\ (Cl R)) \/ ((Cl ((R `) /\ (x `))) /\ (Cl x)) is closed Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

(GX,(GX,R)) is Element of K10( the carrier of GX)

Cl (GX,R) is Element of K10( the carrier of GX)

(GX,R) ` is Element of K10( the carrier of GX)

the carrier of GX \ (GX,R) is set

Cl ((GX,R) `) is Element of K10( the carrier of GX)

(Cl (GX,R)) /\ (Cl ((GX,R) `)) is Element of K10( the carrier of GX)

x is set

Cl ((Cl R) /\ (Cl (R `))) is Element of K10( the carrier of GX)

Cl (Cl R) is Element of K10( the carrier of GX)

Cl (Cl (R `)) is Element of K10( the carrier of GX)

(Cl (Cl R)) /\ (Cl (Cl (R `))) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

x is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

(GX,(R \/ x)) is closed Element of K10( the carrier of GX)

Cl (R \/ x) is closed Element of K10( the carrier of GX)

(R \/ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R \/ x) is set

Cl ((R \/ x) `) is closed Element of K10( the carrier of GX)

(Cl (R \/ x)) /\ (Cl ((R \/ x) `)) is closed Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

(GX,(R /\ x)) is closed Element of K10( the carrier of GX)

Cl (R /\ x) is closed Element of K10( the carrier of GX)

(R /\ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R /\ x) is set

Cl ((R /\ x) `) is closed Element of K10( the carrier of GX)

(Cl (R /\ x)) /\ (Cl ((R /\ x) `)) is closed Element of K10( the carrier of GX)

(GX,(R \/ x)) \/ (GX,(R /\ x)) is closed Element of K10( the carrier of GX)

(GX,x) is closed Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is closed Element of K10( the carrier of GX)

(Cl x) /\ (Cl (x `)) is closed Element of K10( the carrier of GX)

(GX,R) /\ (GX,x) is closed Element of K10( the carrier of GX)

((GX,(R \/ x)) \/ (GX,(R /\ x))) \/ ((GX,R) /\ (GX,x)) is closed Element of K10( the carrier of GX)

x99 is set

(x `) /\ (R `) is Element of K10( the carrier of GX)

Q1 is Element of the carrier of GX

Q1 is Element of K10( the carrier of GX)

(R \/ x) /\ Q1 is Element of K10( the carrier of GX)

((R \/ x) `) /\ Q1 is Element of K10( the carrier of GX)

R /\ Q1 is Element of K10( the carrier of GX)

Q1 /\ x is Element of K10( the carrier of GX)

(R /\ Q1) \/ (Q1 /\ x) is Element of K10( the carrier of GX)

(R `) /\ Q1 is Element of K10( the carrier of GX)

(x `) /\ ((R `) /\ Q1) is Element of K10( the carrier of GX)

Q3 is Element of K10( the carrier of GX)

x /\ Q3 is Element of K10( the carrier of GX)

(x `) ` is Element of K10( the carrier of GX)

the carrier of GX \ (x `) is set

(x `) /\ Q3 is Element of K10( the carrier of GX)

((R `) /\ Q1) /\ ((x `) /\ Q3) is Element of K10( the carrier of GX)

{} /\ Q3 is Element of K10( the carrier of GX)

((R `) /\ Q1) /\ Q3 is Element of K10( the carrier of GX)

Q1 /\ Q3 is Element of K10( the carrier of GX)

(R `) /\ (Q1 /\ Q3) is Element of K10( the carrier of GX)

(x `) \/ (R `) is Element of K10( the carrier of GX)

Q2 is Element of K10( the carrier of GX)

(R /\ x) /\ Q2 is Element of K10( the carrier of GX)

((R /\ x) `) /\ Q2 is Element of K10( the carrier of GX)

R /\ Q2 is Element of K10( the carrier of GX)

(R /\ Q2) /\ x is Element of K10( the carrier of GX)

(R `) /\ Q2 is Element of K10( the carrier of GX)

Q2 /\ (x `) is Element of K10( the carrier of GX)

((R `) /\ Q2) \/ (Q2 /\ (x `)) is Element of K10( the carrier of GX)

Q2 /\ x is Element of K10( the carrier of GX)

R /\ (Q2 /\ x) is Element of K10( the carrier of GX)

(R /\ (Q2 /\ x)) /\ Q3 is Element of K10( the carrier of GX)

(Q2 /\ x) /\ Q3 is Element of K10( the carrier of GX)

R /\ ((Q2 /\ x) /\ Q3) is Element of K10( the carrier of GX)

Q2 /\ (x /\ Q3) is Element of K10( the carrier of GX)

R /\ (Q2 /\ (x /\ Q3)) is Element of K10( the carrier of GX)

Q2 /\ Q3 is Element of K10( the carrier of GX)

R /\ (Q2 /\ Q3) is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

(GX,x) is closed Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

Cl (x `) is closed Element of K10( the carrier of GX)

(Cl x) /\ (Cl (x `)) is closed Element of K10( the carrier of GX)

(GX,R) \/ (GX,x) is closed Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

(GX,(R \/ x)) is closed Element of K10( the carrier of GX)

Cl (R \/ x) is closed Element of K10( the carrier of GX)

(R \/ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R \/ x) is set

Cl ((R \/ x) `) is closed Element of K10( the carrier of GX)

(Cl (R \/ x)) /\ (Cl ((R \/ x) `)) is closed Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

(GX,(R /\ x)) is closed Element of K10( the carrier of GX)

Cl (R /\ x) is closed Element of K10( the carrier of GX)

(R /\ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R /\ x) is set

Cl ((R /\ x) `) is closed Element of K10( the carrier of GX)

(Cl (R /\ x)) /\ (Cl ((R /\ x) `)) is closed Element of K10( the carrier of GX)

(GX,(R \/ x)) \/ (GX,(R /\ x)) is closed Element of K10( the carrier of GX)

(GX,R) /\ (GX,x) is closed Element of K10( the carrier of GX)

((GX,(R \/ x)) \/ (GX,(R /\ x))) \/ ((GX,R) /\ (GX,x)) is closed Element of K10( the carrier of GX)

x99 is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

(GX,(GX,R)) is Element of K10( the carrier of GX)

Cl (GX,R) is Element of K10( the carrier of GX)

(GX,R) ` is Element of K10( the carrier of GX)

the carrier of GX \ (GX,R) is set

Cl ((GX,R) `) is Element of K10( the carrier of GX)

(Cl (GX,R)) /\ (Cl ((GX,R) `)) is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

x is set

Cl ((Cl (R `)) `) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

(GX,(Cl R)) is Element of K10( the carrier of GX)

Cl (Cl R) is Element of K10( the carrier of GX)

(Cl R) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl R) is set

Cl ((Cl R) `) is Element of K10( the carrier of GX)

(Cl (Cl R)) /\ (Cl ((Cl R) `)) is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

(GX,R) is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

((Cl (R `)) `) ` is Element of K10( the carrier of GX)

the carrier of GX \ ((Cl (R `)) `) is set

(Cl R) /\ (((Cl (R `)) `) `) is Element of K10( the carrier of GX)

(Cl R) \ ((Cl (R `)) `) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

(GX,R) is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

R \ (GX,R) is Element of K10( the carrier of GX)

(Cl R) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl R) is set

((Cl (R `)) `) \/ ((Cl R) `) is Element of K10( the carrier of GX)

((Cl R) /\ (Cl (R `))) ` is Element of K10( the carrier of GX)

the carrier of GX \ ((Cl R) /\ (Cl (R `))) is set

R /\ (((Cl (R `)) `) \/ ((Cl R) `)) is Element of K10( the carrier of GX)

R /\ ((Cl R) `) is Element of K10( the carrier of GX)

R /\ (GX,R) is Element of K10( the carrier of GX)

(R /\ ((Cl R) `)) \/ (R /\ (GX,R)) is Element of K10( the carrier of GX)

{} \/ (GX,R) is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

(Cl R) \ (GX,R) is Element of K10( the carrier of GX)

(GX,R) ` is Element of K10( the carrier of GX)

the carrier of GX \ (GX,R) is set

(Cl R) /\ ((GX,R) `) is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

Cl (GX,R) is closed Element of K10( the carrier of GX)

Cl (Cl (R `)) is closed Element of K10( the carrier of GX)

Cl (Cl R) is closed Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

(GX,(GX,R)) is closed Element of K10( the carrier of GX)

Cl (GX,R) is closed Element of K10( the carrier of GX)

(GX,R) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (GX,R) is set

Cl ((GX,R) `) is closed Element of K10( the carrier of GX)

(Cl (GX,R)) /\ (Cl ((GX,R) `)) is closed Element of K10( the carrier of GX)

(GX,(GX,(GX,R))) is open Element of K10( the carrier of GX)

(GX,(GX,R)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (GX,(GX,R)) is set

Cl ((GX,(GX,R)) `) is closed Element of K10( the carrier of GX)

(Cl ((GX,(GX,R)) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((GX,(GX,R)) `)) is set

the Element of (GX,(GX,(GX,R))) is Element of (GX,(GX,(GX,R)))

x99 is Element of the carrier of GX

((GX,R) `) /\ (GX,(GX,(GX,R))) is open Element of K10( the carrier of GX)

((GX,R) `) /\ (GX,R) is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

(GX,(GX,R)) is closed Element of K10( the carrier of GX)

Cl (GX,R) is closed Element of K10( the carrier of GX)

(GX,R) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (GX,R) is set

Cl ((GX,R) `) is closed Element of K10( the carrier of GX)

(Cl (GX,R)) /\ (Cl ((GX,R) `)) is closed Element of K10( the carrier of GX)

(GX,(GX,(GX,R))) is closed Element of K10( the carrier of GX)

Cl (GX,(GX,R)) is closed Element of K10( the carrier of GX)

(GX,(GX,R)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (GX,(GX,R)) is set

Cl ((GX,(GX,R)) `) is closed Element of K10( the carrier of GX)

(Cl (GX,(GX,R))) /\ (Cl ((GX,(GX,R)) `)) is closed Element of K10( the carrier of GX)

(GX,(GX,(GX,R))) is open Element of K10( the carrier of GX)

(Cl ((GX,(GX,R)) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((GX,(GX,R)) `)) is set

(Cl (GX,(GX,R))) \ (GX,(GX,(GX,R))) is Element of K10( the carrier of GX)

GX is set

x is set

R is set

x \ GX is Element of K10(x)

K10(x) is non empty set

x \ R is Element of K10(x)

x99 is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

(Cl R) \ R is Element of K10( the carrier of GX)

(GX,R) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (GX,R) is set

(GX,R) is open Element of K10( the carrier of GX)

(Cl (R `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

(Cl R) \ (GX,R) is Element of K10( the carrier of GX)

R \/ (GX,R) is Element of K10( the carrier of GX)

(R \/ (GX,R)) \ (GX,R) is Element of K10( the carrier of GX)

((GX,R) `) /\ (R \/ (GX,R)) is Element of K10( the carrier of GX)

R /\ ((GX,R) `) is Element of K10( the carrier of GX)

((GX,R) `) /\ (GX,R) is Element of K10( the carrier of GX)

(R /\ ((GX,R) `)) \/ (((GX,R) `) /\ (GX,R)) is Element of K10( the carrier of GX)

R \ (GX,R) is Element of K10( the carrier of GX)

(GX,R) /\ ((GX,R) `) is Element of K10( the carrier of GX)

(R \ (GX,R)) \/ ((GX,R) /\ ((GX,R) `)) is Element of K10( the carrier of GX)

(GX,R) \/ ((GX,R) /\ ((GX,R) `)) is Element of K10( the carrier of GX)

{} GX is empty open closed Element of K10( the carrier of GX)

(GX,R) \/ ({} GX) is open Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

(GX,R) is open Element of K10( the carrier of GX)

(Cl (R `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

R \ (GX,R) is Element of K10( the carrier of GX)

(R `) /\ (GX,R) is Element of K10( the carrier of GX)

(R `) /\ R is Element of K10( the carrier of GX)

{} GX is empty open closed Element of K10( the carrier of GX)

(R `) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R `) is set

(GX,R) ` is closed Element of K10( the carrier of GX)

the carrier of GX \ (GX,R) is set

((R `) `) \/ ((GX,R) `) is Element of K10( the carrier of GX)

((R `) /\ (GX,R)) ` is Element of K10( the carrier of GX)

the carrier of GX \ ((R `) /\ (GX,R)) is set

R \/ (R \ (GX,R)) is Element of K10( the carrier of GX)

((GX,R) `) /\ R is Element of K10( the carrier of GX)

R \/ (((GX,R) `) /\ R) is Element of K10( the carrier of GX)

R \/ ((GX,R) `) is Element of K10( the carrier of GX)

R \/ R is Element of K10( the carrier of GX)

(R \/ ((GX,R) `)) /\ (R \/ R) is Element of K10( the carrier of GX)

({} GX) ` is open closed Element of K10( the carrier of GX)

the carrier of GX \ ({} GX) is set

(({} GX) `) /\ R is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

GX is TopStruct

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

the carrier of GX is set

K10( the carrier of GX) is non empty set

Cl ([#] GX) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

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

Cl x is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

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

x is Element of K10( the carrier of GX)

the Element of x is Element of x

x is set

x99 is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

x /\ R is Element of K10( the carrier of GX)

Cl (x /\ R) is closed Element of K10( the carrier of GX)

x99 is set

Q1 is Element of K10( the carrier of GX)

x /\ Q1 is Element of K10( the carrier of GX)

R /\ (x /\ Q1) is Element of K10( the carrier of GX)

(x /\ R) /\ Q1 is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R /\ x is Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

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

Cl (R /\ x) is closed Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

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

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

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

([#] GX) ` is Element of K10( the carrier of GX)

the carrier of GX \ ([#] GX) is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

{} GX is empty (GX) Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is (GX) Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

(R `) \ x is Element of K10( the carrier of GX)

Cl ((R `) \ x) is closed Element of K10( the carrier of GX)

x ` is Element of K10( the carrier of GX)

the carrier of GX \ x is set

(R `) /\ (x `) is Element of K10( the carrier of GX)

Cl ((R `) /\ (x `)) is closed Element of K10( the carrier of GX)

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

([#] GX) \ x is Element of K10( the carrier of GX)

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl (R `)) \ x is Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

(Cl (R `)) \ (Cl x) is Element of K10( the carrier of GX)

Cl (x `) is closed Element of K10( the carrier of GX)

(R \/ x) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R \/ x) is set

Cl ((R \/ x) `) is closed Element of K10( the carrier of GX)

Cl (Cl ((R \/ x) `)) is closed Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

x is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

x is Element of K10( the carrier of GX)

(R `) /\ x is Element of K10( the carrier of GX)

R /\ ((R `) /\ x) is Element of K10( the carrier of GX)

R /\ (R `) is Element of K10( the carrier of GX)

(R /\ (R `)) /\ x is Element of K10( the carrier of GX)

{} GX is empty open closed (GX) Element of K10( the carrier of GX)

({} GX) /\ x is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

x99 is Element of K10( the carrier of GX)

(R `) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R `) is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

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

(Cl R) /\ ([#] GX) is Element of K10( the carrier of GX)

R \/ (R `) is Element of K10( the carrier of GX)

GX is non empty TopSpace-like TopStruct

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

the carrier of GX is non empty set

K10( the carrier of GX) is non empty set

(GX,([#] GX)) is open Element of K10( the carrier of GX)

([#] GX) ` is open closed Element of K10( the carrier of GX)

the carrier of GX \ ([#] GX) is set

Cl (([#] GX) `) is closed Element of K10( the carrier of GX)

(Cl (([#] GX) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (([#] GX) `)) is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

{} GX is empty open closed (GX) Element of K10( the carrier of GX)

Cl ({} GX) is closed Element of K10( the carrier of GX)

(Cl ({} GX)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ({} GX)) is set

({} GX) ` is open closed Element of K10( the carrier of GX)

the carrier of GX \ ({} GX) is set

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

Cl R is closed Element of K10( the carrier of GX)

(Cl R) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl R) is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

{} GX is empty open closed (GX) (GX) Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

x is Element of K10( the carrier of GX)

R \/ x is Element of K10( the carrier of GX)

Cl x is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

(Cl R) \/ (Cl x) is closed Element of K10( the carrier of GX)

Cl (R \/ x) is closed Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl R is Element of K10( the carrier of GX)

(Cl R) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl R) is set

Cl ((Cl R) `) is Element of K10( the carrier of GX)

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

Cl (R `) is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is (GX) Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

Cl R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is Element of K10( the carrier of GX)

(Cl R) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl R) is set

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

R /\ ([#] GX) is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

R \ (GX,R) is Element of K10( the carrier of GX)

(GX,(Cl R)) is Element of K10( the carrier of GX)

Cl ((Cl R) `) is Element of K10( the carrier of GX)

(Cl ((Cl R) `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((Cl R) `)) is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

(GX,(Cl R)) is open Element of K10( the carrier of GX)

(Cl R) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl R) is set

Cl ((Cl R) `) is closed Element of K10( the carrier of GX)

(Cl ((Cl R) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((Cl R) `)) is set

(GX,R) is open Element of K10( the carrier of GX)

(Cl (R `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

R /\ (GX,R) is Element of K10( the carrier of GX)

{} GX is empty open closed (GX) (GX) Element of K10( the carrier of GX)

(GX,(R /\ (GX,R))) is open Element of K10( the carrier of GX)

(R /\ (GX,R)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R /\ (GX,R)) is set

Cl ((R /\ (GX,R)) `) is closed Element of K10( the carrier of GX)

(Cl ((R /\ (GX,R)) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((R /\ (GX,R)) `)) is set

(GX,(GX,R)) is open Element of K10( the carrier of GX)

(GX,R) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (GX,R) is set

Cl ((GX,R) `) is closed Element of K10( the carrier of GX)

(Cl ((GX,R) `)) ` is open Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((GX,R) `)) is set

R /\ (GX,(GX,R)) is Element of K10( the carrier of GX)

the Element of (GX,(GX,R)) is Element of (GX,(GX,R))

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is open Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is closed Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

(GX,(R `)) is closed Element of K10( the carrier of GX)

(R `) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R `) is set

Cl ((R `) `) is closed Element of K10( the carrier of GX)

(Cl (R `)) /\ (Cl ((R `) `)) is closed Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is closed Element of K10( the carrier of GX)

(GX,R) is closed Element of K10( the carrier of GX)

Cl R is closed Element of K10( the carrier of GX)

R ` is open Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is closed Element of K10( the carrier of GX)

(Cl R) /\ (Cl (R `)) is closed Element of K10( the carrier of GX)

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

GX is TopSpace-like TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl R is Element of K10( the carrier of GX)

(GX,(Cl R)) is Element of K10( the carrier of GX)

(Cl R) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl R) is set

Cl ((Cl R) `) is Element of K10( the carrier of GX)

(Cl ((Cl R) `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((Cl R) `)) is set

(GX,(R `)) is Element of K10( the carrier of GX)

(R `) ` is Element of K10( the carrier of GX)

the carrier of GX \ (R `) is set

Cl ((R `) `) is Element of K10( the carrier of GX)

(Cl ((R `) `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl ((R `) `)) is set

Cl (GX,(R `)) is Element of K10( the carrier of GX)

GX is TopStruct

the carrier of GX is set

K10( the carrier of GX) is non empty set

R is Element of K10( the carrier of GX)

(GX,R) is Element of K10( the carrier of GX)

R ` is Element of K10( the carrier of GX)

the carrier of GX \ R is set

Cl (R `) is Element of K10( the carrier of GX)

(Cl (R `)) ` is Element of K10( the carrier of GX)

the carrier of GX \ (Cl (R `)) is set

(GX,(GX,R)) is Element of K10( the carrier of GX)