:: 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)
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)
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 (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)
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,(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)
(Cl R) \ 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)
the carrier of GX \ (Cl ((Cl 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)
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
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)
x99 is Element of K10( the carrier of R)
Cl 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
Cl (R,x99) is Element of K10( the carrier of R)
(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
(GX,(GX,x)) is closed (GX) (GX) Element of K10( the carrier of GX)
Cl (GX,x) is closed Element of K10( the carrier of GX)
(GX,x) ` is closed Element of K10( the carrier of GX)
the carrier of GX \ (GX,x) is set
Cl ((GX,x) `) is closed Element of K10( the carrier of GX)
(Cl (GX,x)) /\ (Cl ((GX,x) `)) is closed Element of K10( the carrier of GX)
(GX,(GX,x)) is open Element of K10( the carrier of GX)
(Cl ((GX,x) `)) ` is open Element of K10( the carrier of GX)
the carrier of GX \ (Cl ((GX,x) `)) is set
(Cl (GX,x)) \ (GX,(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)
(Cl x) /\ (Cl (x `)) is closed Element of K10( the carrier of GX)
x \ (GX,x) is Element of K10( the carrier of GX)
(GX,(Cl x)) is open 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
Cl ((Cl x) `) is closed Element of K10( the carrier of GX)
(Cl ((Cl x) `)) ` is open Element of K10( the carrier of GX)
the carrier of GX \ (Cl ((Cl 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 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)
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
Cl x99 is Element of K10( the carrier of R)
(R,(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
Cl ((Cl x99) `) is Element of K10( the carrier of R)
(Cl ((Cl x99) `)) ` is Element of K10( the carrier of R)
the carrier of R \ (Cl ((Cl x99) `)) is set
Cl x is closed Element of K10( the carrier of GX)
(GX,(Cl x)) is closed (GX) (GX) Element of K10( the carrier of GX)
Cl (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
Cl ((Cl x) `) is closed Element of K10( the carrier of GX)
(Cl (Cl x)) /\ (Cl ((Cl x) `)) is closed Element of K10( the carrier of GX)
(Cl x) \ x is Element of K10( the carrier of GX)
(GX,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,x) is open 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
Cl (GX,x) is closed Element of K10( the carrier of GX)
(GX,(Cl x)) is open Element of K10( the carrier of GX)
(Cl ((Cl x) `)) ` is open Element of K10( the carrier of GX)
the carrier of GX \ (Cl ((Cl 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)
x is Element of K10( the carrier of GX)
R \/ 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
Cl (GX,x) is closed 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
Cl (GX,R) is closed Element of K10( the carrier of GX)
(GX,R) \/ (GX,x) is open Element of K10( the carrier of GX)
Cl ((GX,R) \/ (GX,x)) is closed Element of K10( the carrier of GX)
(GX,(R \/ x)) is open 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 (GX,(R \/ x)) is closed Element of K10( the carrier of GX)
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)
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
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)
(R /\ x) ` is Element of K10( the carrier of GX)
the carrier of GX \ (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 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 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
the Element of (GX,(GX,R)) is Element of (GX,(GX,R))
(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 (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
(Cl R) ` is open Element of K10( the carrier of GX)
the carrier of GX \ (Cl R) is set
((Cl R) `) \/ ((Cl (R `)) `) is open Element of K10( the carrier of GX)
Cl (((Cl R) `) \/ ((Cl (R `)) `)) is closed Element of K10( the carrier of GX)
(Cl (((Cl R) `) \/ ((Cl (R `)) `))) ` is open Element of K10( the carrier of GX)
the carrier of GX \ (Cl (((Cl R) `) \/ ((Cl (R `)) `))) is set
Cl ((Cl 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) `)) \/ (Cl ((Cl (R `)) `)) is closed Element of K10( the carrier of GX)
((Cl ((Cl R) `)) \/ (Cl ((Cl (R `)) `))) ` is open Element of K10( the carrier of GX)
the carrier of GX \ ((Cl ((Cl R) `)) \/ (Cl ((Cl (R `)) `))) is set
(GX,(Cl R)) is open 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,(Cl R)) /\ ((Cl (GX,R)) `) is open Element of K10( 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)
(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 R is Element of K10( the carrier of GX)
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
(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 ((Cl ((Cl R) `)) `) is Element of K10( the carrier of GX)
Cl (Cl (GX,R)) is Element of K10( the carrier of GX)
Cl (GX,(Cl R)) is Element of K10( the carrier of GX)
(GX,(GX,(Cl R))) is Element of K10( the carrier of GX)
(GX,(Cl R)) ` is Element of K10( the carrier of GX)
the carrier of GX \ (GX,(Cl R)) is set
Cl ((GX,(Cl R)) `) is Element of K10( the carrier of GX)
(Cl ((GX,(Cl R)) `)) ` is Element of K10( the carrier of GX)
the carrier of GX \ (Cl ((GX,(Cl R)) `)) is set
(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 (GX,(GX,R)) is Element of K10( the carrier of GX)
Cl (Cl R) is Element of K10( the carrier of GX)
(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
Cl ((Cl (Cl R)) `) is Element of K10( the carrier of GX)
(Cl ((Cl (Cl R)) `)) ` is Element of K10( the carrier of GX)
the carrier of GX \ (Cl ((Cl (Cl R)) `)) is set