:: TEX_4 semantic presentation

K122() is Element of bool K118()
K118() is set
bool K118() is non empty set
K96() is set
bool K96() is non empty set
bool K122() is non empty set
2 is non empty set
[:2,2:] is non empty set
[:[:2,2:],2:] is non empty set
bool [:[:2,2:],2:] is non empty set
K251() is non empty strict TopSpace-like TopStruct
the carrier of K251() is non empty set
{} is empty trivial set
the empty trivial set is empty trivial set
1 is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
Cl X0 is closed Element of bool the carrier of X
X is TopSpace-like TopStruct
the carrier of X is set
bool the carrier of X is non empty set
X0 is empty trivial open closed boundary nowhere_dense Element of bool the carrier of X
Cl X0 is closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty non proper Element of bool the carrier of X
Cl X0 is non empty closed Element of bool the carrier of X
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
X is non empty non trivial TopSpace-like TopStruct
the carrier of X is non empty non trivial set
bool the carrier of X is non empty set
X0 is non empty non trivial Element of bool the carrier of X
Cl X0 is non empty closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
Cl X0 is closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is closed & X0 c= b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is closed & X0 c= b₁ ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
D is set
A1 is Element of bool the carrier of X
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
A1 is set
D is non empty Element of bool (bool the carrier of X)
A2 is Element of bool the carrier of X
meet D is Element of bool the carrier of X
A1 is Element of bool the carrier of X
A2 is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is closed & X0 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is closed & X0 in b₁ ) } is set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is closed & {X0} c= b₁ ) } is set
A1 is set
A2 is Element of bool the carrier of X
A1 is set
A2 is Element of bool the carrier of X
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is closed & {X0} c= b₁ ) } is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty non proper Element of bool the carrier of X
Int X0 is open Element of bool the carrier of X
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is proper Element of bool the carrier of X
Int X0 is open Element of bool the carrier of X
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is empty trivial proper open closed boundary nowhere_dense Element of bool the carrier of X
Int X0 is empty trivial proper open closed boundary nowhere_dense Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
Int X0 is open Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & b₁ c= X0 ) } is set
union { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & b₁ c= X0 ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
D is set
A1 is Element of bool the carrier of X
{} X is empty trivial proper open closed boundary nowhere_dense Element of bool the carrier of X
A1 is set
D is non empty Element of bool (bool the carrier of X)
A2 is Element of bool the carrier of X
union D is Element of bool the carrier of X
A1 is Element of bool the carrier of X
A2 is Element of bool the carrier of X
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
[#] X is non empty non proper dense Element of bool the carrier of X
D is Element of bool the carrier of X
([#] X) \ D is Element of bool the carrier of X
X0 \ D is Element of bool the carrier of X
A is Element of the carrier of X
A2 is set
(([#] X) \ D) ` is Element of bool the carrier of X
the carrier of X \ (([#] X) \ D) is set
D ` is Element of bool the carrier of X
the carrier of X \ D is set
(D `) ` is Element of bool the carrier of X
the carrier of X \ (D `) is set
X0 /\ D is Element of bool the carrier of X
D is Element of bool the carrier of X
([#] X) \ D is Element of bool the carrier of X
X0 \ D is Element of bool the carrier of X
([#] X) \ (([#] X) \ D) is Element of bool the carrier of X
A is Element of the carrier of X
A2 is set
D ` is Element of bool the carrier of X
the carrier of X \ D is set
(([#] X) \ D) ` is Element of bool the carrier of X
the carrier of X \ (([#] X) \ D) is set
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of bool the carrier of X
X0 /\ A is Element of bool the carrier of X
D is set
A1 is Element of the carrier of X
D is Element of bool the carrier of X
A is Element of the carrier of X
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of bool the carrier of X
[#] X is non proper dense Element of bool the carrier of X
([#] X) \ A is Element of bool the carrier of X
A ` is Element of bool the carrier of X
the carrier of X \ A is set
(A `) ` is Element of bool the carrier of X
the carrier of X \ (A `) is set
A is Element of bool the carrier of X
([#] X) \ A is Element of bool the carrier of X
([#] X) \ (([#] X) \ A) is Element of bool the carrier of X
A ` is Element of bool the carrier of X
the carrier of X \ A is set
(A `) ` is Element of bool the carrier of X
the carrier of X \ (A `) is set
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
X0 is TopStruct
the carrier of X0 is set
bool the carrier of X0 is non empty set
the topology of X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is strict TopStruct
the topology of X0 is Element of bool (bool the carrier of X0)
bool (bool the carrier of X0) is non empty set
TopStruct(# the carrier of X0, the topology of X0 #) is strict TopStruct
A is Element of bool the carrier of X
D is Element of bool the carrier of X0
A1 is Element of bool the carrier of X0
A2 is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
A is Element of bool the carrier of X
X0 is Element of bool the carrier of X
D is Element of bool the carrier of X
A /\ D is Element of bool the carrier of X
X0 /\ D is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
{X0} is non empty trivial Element of bool the carrier of X
bool the carrier of X is non empty set
A is Element of bool the carrier of X
{X0} /\ A is Element of bool the carrier of X
D is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is empty trivial proper boundary Element of bool the carrier of X
A is Element of bool the carrier of X
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
X0 is Element of bool (bool the carrier of X)
meet X0 is Element of bool the carrier of X
union X0 is Element of bool the carrier of X
A is Element of bool the carrier of X
D is set
A1 is Element of bool the carrier of X
A2 is set
A1 is Element of bool the carrier of X
A1 /\ A is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
X0 is Element of bool (bool the carrier of X)
meet X0 is Element of bool the carrier of X
union X0 is Element of bool the carrier of X
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
bool (bool the carrier of X) is non empty set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
D is set
A1 is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
{X0} is non empty trivial Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
A is Element of bool the carrier of X
D is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
{X0} is non empty trivial Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
meet (X,X0) is Element of bool the carrier of X
A is set
D is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
{X0} is non empty trivial Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
meet (X,X0) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial Element of bool the carrier of X
meet (X,X0) is Element of bool the carrier of X
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
X0 is TopStruct
the carrier of X0 is set
bool the carrier of X0 is non empty set
the topology of X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is strict TopStruct
the topology of X0 is Element of bool (bool the carrier of X0)
bool (bool the carrier of X0) is non empty set
TopStruct(# the carrier of X0, the topology of X0 #) is strict TopStruct
A is Element of bool the carrier of X
D is Element of bool the carrier of X0
A1 is Element of bool the carrier of X0
A2 is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is set
D is empty trivial proper boundary Element of bool the carrier of X
A is Element of the carrier of X
{A} is non empty trivial Element of bool the carrier of X
A1 is non empty trivial Element of bool the carrier of X
A1 is non empty trivial Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
A is Element of bool the carrier of X
A /\ X0 is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
A is Element of bool the carrier of X
A /\ X0 is Element of bool the carrier of X
X is TopStruct
the carrier of X is set
X0 is Element of the carrier of X
(X,X0) is Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
{X0} is non empty trivial Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
A is Element of bool the carrier of X
{X0} is non empty trivial Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
A is Element of the carrier of X
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
(X,X0) /\ (X,A) is Element of bool the carrier of X
D is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is closed & X0 in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is closed & X0 in b<sub>1</sub> ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
D is set
A1 is Element of bool the carrier of X
A1 is set
D is Element of bool (bool the carrier of X)
A2 is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
D is set
A1 is Element of bool the carrier of X
A1 is set
D is Element of bool (bool the carrier of X)
A2 is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is set
D is Element of the carrier of X
(X,D) is non empty Element of bool the carrier of X
(X,D) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & D in b<sub>1</sub> ) } is set
union (X,D) is Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
D is Element of the carrier of X
(X,D) is non empty Element of bool the carrier of X
(X,D) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & D in b<sub>1</sub> ) } is set
union (X,D) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
A is set
D is Element of the carrier of X
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
D is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
D is Element of bool (bool the carrier of X)
union D is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial Element of bool the carrier of X
(X,{X0}) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in {X0} } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in {X0} } is set
D is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
(X,A) /\ (X,X0) is Element of bool the carrier of X
A1 is set
A2 is Element of the carrier of X
A1 is set
(X,A2) is non empty Element of bool the carrier of X
(X,A2) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A2 in b<sub>1</sub> ) } is set
union (X,A2) is Element of bool the carrier of X
R is Element of the carrier of X
(X,R) is non empty Element of bool the carrier of X
(X,R) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & R in b<sub>1</sub> ) } is set
union (X,R) is Element of bool the carrier of X
{R} is non empty trivial Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
(X,A) /\ X0 is Element of bool the carrier of X
A1 is set
A2 is Element of the carrier of X
{A2} is non empty trivial Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in {A2} } is set
R is set
c<sub>9</sub> is Element of the carrier of X
(X,c<sub>9</sub>) is non empty Element of bool the carrier of X
(X,c<sub>9</sub>) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & c<sub>9</sub> in b<sub>1</sub> ) } is set
union (X,c<sub>9</sub>) is Element of bool the carrier of X
(X,{A2}) is Element of bool the carrier of X
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in {A2} } is set
(X,A2) is non empty Element of bool the carrier of X
(X,A2) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A2 in b<sub>1</sub> ) } is set
union (X,A2) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
(X,A) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
A2 is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
A is set
D is Element of the carrier of X
{D} is non empty trivial Element of bool the carrier of X
(X,{D}) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in {D} } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in {D} } is set
(X,D) is non empty Element of bool the carrier of X
(X,D) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & D in b<sub>1</sub> ) } is set
union (X,D) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
(X,(X,X0)) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in (X,X0) } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in (X,X0) } is set
A is set
D is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
A2 is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of bool the carrier of X
(X,A) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
(X,(X,A)) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in (X,A) } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in (X,A) } is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
A is Element of bool the carrier of X
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
(X,A) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of bool the carrier of X
X0 \/ A is Element of bool the carrier of X
(X,(X0 \/ A)) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 \/ A } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 \/ A } is set
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
(X,A) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
(X,X0) \/ (X,A) is Element of bool the carrier of X
D is set
A1 is set
A2 is Element of the carrier of X
(X,A2) is non empty Element of bool the carrier of X
(X,A2) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A2 in b<sub>1</sub> ) } is set
union (X,A2) is Element of bool the carrier of X
A1 is set
A1 is set
A1 is set
A1 is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of bool the carrier of X
X0 /\ A is Element of bool the carrier of X
(X,(X0 /\ A)) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 /\ A } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 /\ A } is set
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
(X,A) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
(X,X0) /\ (X,A) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is empty trivial proper boundary Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
A is set
D is Element of the carrier of X
A1 is set
A2 is Element of the carrier of X
(X,A2) is non empty Element of bool the carrier of X
(X,A2) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A2 in b<sub>1</sub> ) } is set
union (X,A2) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty non proper Element of bool the carrier of X
(X,X0) is non empty Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
X is non empty non trivial TopStruct
the carrier of X is non empty non trivial set
bool the carrier of X is non empty set
X0 is non empty non trivial Element of bool the carrier of X
(X,X0) is non empty Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of bool the carrier of X
(X,A) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
D is set
A1 is Element of the carrier of X
A2 is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
{A1} is non empty trivial Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 c= b<sub>1</sub> ) } is set
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 c= b<sub>1</sub> ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
D is set
A1 is Element of bool the carrier of X
A1 is set
D is Element of bool (bool the carrier of X)
A2 is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of bool the carrier of X
(X,A) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in A } is set
D is set
A1 is Element of the carrier of X
A2 is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A1 in b<sub>1</sub> ) } is set
union (X,A1) is Element of bool the carrier of X
{A1} is non empty trivial Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is closed & X0 c= b<sub>1</sub> ) } is set
(X,X0) is Element of bool the carrier of X
{ (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (X,b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is closed & X0 c= b<sub>1</sub> ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
D is set
A1 is Element of bool the carrier of X
A1 is set
D is Element of bool (bool the carrier of X)
A2 is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
A is Element of bool the carrier of X
X0 /\ A is Element of bool the carrier of X
D is set
A1 is Element of the carrier of X
{A1} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A1} is non empty closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
Cl X0 is closed Element of bool the carrier of X
A is Element of the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
A is Element of the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of the carrier of X
D is Element of the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
{D} is non empty trivial V170(X) Element of bool the carrier of X
Cl {D} is non empty closed Element of bool the carrier of X
A is Element of the carrier of X
D is set
A1 is Element of the carrier of X
{A1} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A1} is non empty closed Element of bool the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
A is Element of bool the carrier of X
A /\ (Cl {X0}) is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
A is Element of the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
A is Element of the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
A is set
D is Element of the carrier of X
{D} is non empty trivial V170(X) Element of bool the carrier of X
Cl {D} is non empty closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
Int X0 is open Element of bool the carrier of X
X0 /\ (Int X0) is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
bool the carrier of X is non empty set
Cl {X0} is non empty closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
D is set
A1 is Element of bool the carrier of X
A1 is set
D is Element of bool (bool the carrier of X)
A2 is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is closed & X0 in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is closed & X0 in b<sub>1</sub> ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
D is set
A1 is Element of bool the carrier of X
A1 is set
D is Element of bool (bool the carrier of X)
A2 is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is closed & X0 in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is closed & X0 in b<sub>1</sub> ) } is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
(X,X0) \/ (X,A) is non empty Element of bool the carrier of X
D is Element of the carrier of X
(X,D) is non empty Element of bool the carrier of X
(X,D) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & D in b<sub>1</sub> ) } is set
union (X,D) is Element of bool the carrier of X
{D} is non empty trivial V170(X) Element of bool the carrier of X
Cl {D} is non empty closed Element of bool the carrier of X
(X,D) is non empty Element of bool the carrier of X
(X,D) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & D in b<sub>1</sub> ) } is set
union (X,D) is Element of bool the carrier of X
{D} is non empty trivial V170(X) Element of bool the carrier of X
Cl {D} is non empty closed Element of bool the carrier of X
{D} is non empty trivial V170(X) Element of bool the carrier of X
Cl {D} is non empty closed Element of bool the carrier of X
{D} is non empty trivial V170(X) Element of bool the carrier of X
Cl {D} is non empty closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } is set
(Cl {X0}) /\ (meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } ) is Element of bool the carrier of X
bool the carrier of X is non empty Element of bool (bool the carrier of X)
D is set
A1 is Element of bool the carrier of X
D is Element of bool (bool the carrier of X)
meet D is Element of bool the carrier of X
(Cl {X0}) /\ (meet D) is Element of bool the carrier of X
((Cl {X0}) /\ (meet D)) \ (X,X0) is Element of bool the carrier of X
A1 is set
A2 is Element of the carrier of X
(X,A2) is non empty Element of bool the carrier of X
(X,A2) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A2 in b<sub>1</sub> ) } is set
union (X,A2) is Element of bool the carrier of X
{A2} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A2} is non empty closed Element of bool the carrier of X
(Cl {A2}) ` is open Element of bool the carrier of X
the carrier of X \ (Cl {A2}) is set
A1 is non empty Element of bool the carrier of X
A2 is non empty Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
A is Element of the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } is set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 in b₁ ) } is set
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
A2 is set
A1 is Element of bool the carrier of X
(Cl {A}) ` is open Element of bool the carrier of X
the carrier of X \ (Cl {A}) is set
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
(Cl {A}) /\ (meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & A in b<sub>1</sub> ) } ) is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
A is Element of the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & A in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & A in b<sub>1</sub> ) } is set
(Cl {A}) /\ (meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & A in b<sub>1</sub> ) } ) is Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
A1 is set
A2 is Element of bool the carrier of X
A1 is set
R is Element of bool the carrier of X
A1 is Element of bool (bool the carrier of X)
meet A1 is Element of bool the carrier of X
A1 is Element of bool (bool the carrier of X)
meet A1 is Element of bool the carrier of X
(Cl {A}) /\ (meet A1) is Element of bool the carrier of X
A1 is Element of bool (bool the carrier of X)
meet A1 is Element of bool the carrier of X
(Cl {A}) ` is open Element of bool the carrier of X
the carrier of X \ (Cl {A}) is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & X0 in b₁ ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 in b₁ ) } is set
(Cl {X0}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 in b₁ ) } ) is Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A in b₁ ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } is set
(Cl {A}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } ) is Element of bool the carrier of X
(Cl {A}) ` is open Element of bool the carrier of X
the carrier of X \ (Cl {A}) is set
(Cl {X0}) ` is open Element of bool the carrier of X
the carrier of X \ (Cl {X0}) is set
(X,X0) /\ (X,A) is Element of bool the carrier of X
A2 is open Element of bool the carrier of X
(X,X0) \ ((Cl {A}) `) is Element of bool the carrier of X
A1 is set
R is Element of the carrier of X
{R} is non empty trivial V170(X) Element of bool the carrier of X
(X,R) is non empty Element of bool the carrier of X
(X,R) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & R in b<sub>1</sub> ) } is set
union (X,R) is Element of bool the carrier of X
Cl {R} is non empty closed Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & R in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & R in b<sub>1</sub> ) } is set
(Cl {R}) /\ (meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & R in b<sub>1</sub> ) } ) is Element of bool the carrier of X
(X,A) \ A2 is Element of bool the carrier of X
c<sub>9</sub> is set
a is Element of the carrier of X
{a} is non empty trivial V170(X) Element of bool the carrier of X
(X,a) is non empty Element of bool the carrier of X
(X,a) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & a in b<sub>1</sub> ) } is set
union (X,a) is Element of bool the carrier of X
Cl {a} is non empty closed Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & a in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & a in b<sub>1</sub> ) } is set
(Cl {a}) /\ (meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & a in b<sub>1</sub> ) } ) is Element of bool the carrier of X
A2 is open Element of bool the carrier of X
D is Element of bool the carrier of X
D is Element of bool the carrier of X
D /\ (X,A) is Element of bool the carrier of X
D is Element of bool the carrier of X
D is Element of bool the carrier of X
D /\ (X,X0) is Element of bool the carrier of X
D is Element of bool the carrier of X
A1 is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & X0 in b<sub>1</sub> ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } is set
(Cl {X0}) /\ (meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & X0 in b<sub>1</sub> ) } ) is Element of bool the carrier of X
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is (X) & A in b<sub>1</sub> ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & A in b<sub>1</sub> ) } is set
meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & A in b<sub>1</sub> ) } is set
(Cl {A}) /\ (meet { b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of X : ( b<sub>1</sub> is open & A in b<sub>1</sub> ) } ) is Element of bool the carrier of X
D is Element of bool the carrier of X
D is Element of bool the carrier of X
D ` is Element of bool the carrier of X
the carrier of X \ D is set
A1 is Element of bool the carrier of X
A1 is Element of bool the carrier of X
D is Element of bool the carrier of X
D is Element of bool the carrier of X
D ` is Element of bool the carrier of X
the carrier of X \ D is set
A1 is Element of bool the carrier of X
A1 is Element of bool the carrier of X
D is Element of bool the carrier of X
D is Element of bool the carrier of X
D /\ (X,A) is Element of bool the carrier of X
D is Element of bool the carrier of X
D is Element of bool the carrier of X
D /\ (X,X0) is Element of bool the carrier of X
D is Element of bool the carrier of X
A1 is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 c= b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 c= b₁ ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
D is set
A1 is Element of bool the carrier of X
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
D is Element of bool (bool the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 c= b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 c= b₁ ) } is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
Int X0 is open Element of bool the carrier of X
(X,(Int X0)) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in Int X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in Int X0 } is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is closed & X0 c= b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is closed & X0 c= b₁ ) } is set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
D is set
A1 is Element of bool the carrier of X
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
D is Element of bool (bool the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
Cl X0 is closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is closed & X0 c= b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is closed & X0 c= b₁ ) } is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
Cl X0 is closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
Cl X0 is closed Element of bool the carrier of X
(X,(Cl X0)) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in Cl X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in Cl X0 } is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
Cl (X,X0) is closed Element of bool the carrier of X
Cl X0 is closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
Cl X0 is closed Element of bool the carrier of X
A is Element of bool the carrier of X
(X,A) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
Cl A is closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
A is Element of bool the carrier of X
X0 /\ A is Element of bool the carrier of X
(X,(X0 /\ A)) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 /\ A } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 /\ A } is set
(X,A) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
(X,X0) /\ (X,A) is Element of bool the carrier of X
D is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A1 in b₁ ) } is set
union (X,A1) is Element of bool the carrier of X
{A1} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A1} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
(Cl {A1}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } ) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
A2 is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A1 in b₁ ) } is set
union (X,A1) is Element of bool the carrier of X
{A1} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A1} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
(Cl {A1}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } ) is Element of bool the carrier of X
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A1 in b₁ ) } is set
union (X,A1) is Element of bool the carrier of X
{A1} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A1} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
(Cl {A1}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } ) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
A2 is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A1 in b₁ ) } is set
union (X,A1) is Element of bool the carrier of X
{A1} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A1} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
(Cl {A1}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } ) is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
A is Element of bool the carrier of X
X0 /\ A is Element of bool the carrier of X
(X,(X0 /\ A)) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 /\ A } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 /\ A } is set
(X,A) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
(X,X0) /\ (X,A) is Element of bool the carrier of X
D is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A1 in b₁ ) } is set
union (X,A1) is Element of bool the carrier of X
{A1} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A1} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
(Cl {A1}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } ) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
A2 is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A1 in b₁ ) } is set
union (X,A1) is Element of bool the carrier of X
{A1} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A1} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
(Cl {A1}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } ) is Element of bool the carrier of X
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A1 in b₁ ) } is set
union (X,A1) is Element of bool the carrier of X
{A1} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A1} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
(Cl {A1}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } ) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
A2 is set
A1 is Element of the carrier of X
(X,A1) is non empty Element of bool the carrier of X
(X,A1) is non empty Element of bool (bool the carrier of X)
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A1 in b₁ ) } is set
union (X,A1) is Element of bool the carrier of X
{A1} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A1} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } is set
(Cl {A1}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A1 in b₁ ) } ) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is SubSpace of X
the carrier of X0 is set
A is Element of bool the carrier of X
the topology of X0 is Element of bool (bool the carrier of X0)
bool the carrier of X0 is non empty set
bool (bool the carrier of X0) is non empty set
{{}, the carrier of X0} is non empty set
D is Element of bool the carrier of X
A /\ D is Element of bool the carrier of X
A2 is Element of bool the carrier of X
the topology of X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
A1 is Element of bool the carrier of X0
[#] X0 is non proper dense Element of bool the carrier of X0
A2 /\ ([#] X0) is Element of bool the carrier of X0
A2 is Element of bool the carrier of X
A2 /\ ([#] X0) is Element of bool the carrier of X0
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is SubSpace of X
the carrier of X0 is set
the topology of X0 is Element of bool (bool the carrier of X0)
bool the carrier of X0 is non empty set
bool (bool the carrier of X0) is non empty set
A is Element of bool the carrier of X
D is set
the topology of X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
A1 is Element of bool the carrier of X0
[#] X0 is non proper dense Element of bool the carrier of X0
A2 is Element of bool the carrier of X
A2 /\ ([#] X0) is Element of bool the carrier of X0
A1 is Element of bool the carrier of X
{{}, the carrier of X0} is non empty set
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
bool the carrier of X is non empty set
the carrier of X0 is non empty set
D is Element of bool the carrier of X
A is Element of bool the carrier of X
A1 is non empty strict TopSpace-like open SubSpace of X
the carrier of A1 is non empty set
A is Element of bool the carrier of X
A is Element of bool the carrier of X
A is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
bool the carrier of X is non empty set
the carrier of X0 is non empty set
D is Element of bool the carrier of X
A is Element of bool the carrier of X
A1 is non empty strict TopSpace-like closed SubSpace of X
the carrier of A1 is non empty set
A is Element of bool the carrier of X
A is Element of bool the carrier of X
A is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like anti-discrete almost_discrete SubSpace of X
the carrier of X is non empty set
bool the carrier of X is non empty set
the carrier of X0 is set
D is TopSpace-like open SubSpace of X
the carrier of D is set
A1 is Element of bool the carrier of X
A is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like anti-discrete almost_discrete SubSpace of X
the carrier of X is non empty set
bool the carrier of X is non empty set
the carrier of X0 is set
D is TopSpace-like closed SubSpace of X
the carrier of D is set
A1 is Element of bool the carrier of X
A is Element of bool the carrier of X
X is non empty TopStruct
X is non empty TopStruct
X0 is SubSpace of X
X0 is SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty TopSpace-like SubSpace of X
the carrier of X0 is non empty set
A is Element of bool the carrier of X
D is Element of bool the carrier of X
A1 is non empty strict TopSpace-like SubSpace of X
the carrier of A1 is non empty set
D is TopSpace-like SubSpace of X
the carrier of D is set
A1 is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
bool the carrier of X is non empty set
the carrier of X0 is non empty set
A is Element of bool the carrier of X
X0 is non empty TopSpace-like SubSpace of X
X0 is non empty TopSpace-like SubSpace of X
X0 is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
bool the carrier of X is non empty set
the carrier of X0 is non empty set
A is Element of bool the carrier of X
X0 is non empty TopSpace-like SubSpace of X
X0 is non empty TopSpace-like SubSpace of X
X is TopStruct
the carrier of X is set
X0 is Element of the carrier of X
(X,X0) is Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & X0 in b₁ ) } is set
union (X,X0) is Element of bool the carrier of X
X | (X,X0) is strict SubSpace of X
the carrier of (X | (X,X0)) is set
[#] (X | (X,X0)) is non proper dense Element of bool the carrier of (X | (X,X0))
bool the carrier of (X | (X,X0)) is non empty set
A is strict SubSpace of X
the carrier of A is set
D is strict SubSpace of X
the carrier of D is set
[#] D is non proper dense Element of bool the carrier of D
bool the carrier of D is non empty set
[#] A is non proper dense Element of bool the carrier of A
bool the carrier of A is non empty set
[#] X is non proper dense Element of bool the carrier of X
A1 is Element of bool the carrier of X
X | A1 is strict SubSpace of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is strict SubSpace of X
the carrier of (X,X0) is set
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & X0 in b₁ ) } is set
union (X,X0) is Element of bool the carrier of X
X is non empty TopStruct
X0 is SubSpace of X
the carrier of X0 is set
A is SubSpace of X
the carrier of A is set
[#] X0 is non proper dense Element of bool the carrier of X0
bool the carrier of X0 is non empty set
[#] A is non proper dense Element of bool the carrier of A
bool the carrier of A is non empty set
the topology of X0 is Element of bool (bool the carrier of X0)
bool (bool the carrier of X0) is non empty set
the topology of A is Element of bool (bool the carrier of A)
bool (bool the carrier of A) is non empty set
A2 is Element of bool the carrier of X0
the carrier of X is non empty set
bool the carrier of X is non empty set
the topology of X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
A1 is Element of bool the carrier of X
A1 /\ the carrier of X0 is Element of bool the carrier of X
A1 /\ the carrier of A is Element of bool the carrier of X
R is Element of bool the carrier of A
R /\ the carrier of X0 is Element of bool the carrier of A
the carrier of A /\ the carrier of X0 is set
A1 /\ ( the carrier of A /\ the carrier of X0) is Element of bool the carrier of X
A1 is Element of bool the carrier of A
A1 /\ the carrier of X0 is Element of bool the carrier of A
the carrier of X is non empty set
bool the carrier of X is non empty set
the topology of X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
R is Element of bool the carrier of X
R /\ ([#] A) is Element of bool the carrier of A
the carrier of A /\ the carrier of X0 is set
R /\ ( the carrier of A /\ the carrier of X0) is Element of bool the carrier of X
R /\ the carrier of X0 is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
Sspace X0 is non empty trivial V46() V51(1) strict SubSpace of X
(X,X0) is non empty strict SubSpace of X
the carrier of (Sspace X0) is non empty trivial V31() set
{X0} is non empty trivial Element of bool the carrier of X
bool the carrier of X is non empty set
the carrier of (X,X0) is non empty set
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & X0 in b₁ ) } is set
union (X,X0) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
A is Element of the carrier of X
X0 is Element of the carrier of X
(X,X0) is non empty strict SubSpace of X
the carrier of (X,X0) is non empty set
(X,A) is non empty strict SubSpace of X
the carrier of (X,A) is non empty set
the topology of (X,A) is Element of bool (bool the carrier of (X,A))
bool the carrier of (X,A) is non empty set
bool (bool the carrier of (X,A)) is non empty set
TopStruct(# the carrier of (X,A), the topology of (X,A) #) is non empty strict TopStruct
the topology of (X,X0) is Element of bool (bool the carrier of (X,X0))
bool the carrier of (X,X0) is non empty set
bool (bool the carrier of (X,X0)) is non empty set
TopStruct(# the carrier of (X,X0), the topology of (X,X0) #) is non empty strict TopStruct
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & X0 in b₁ ) } is set
union (X,X0) is Element of bool the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A in b₁ ) } is set
union (X,A) is Element of bool the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A in b₁ ) } is set
union (X,A) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty strict SubSpace of X
the carrier of (X,X0) is non empty set
A is Element of the carrier of X
(X,A) is non empty strict SubSpace of X
the carrier of (X,A) is non empty set
the topology of (X,X0) is Element of bool (bool the carrier of (X,X0))
bool the carrier of (X,X0) is non empty set
bool (bool the carrier of (X,X0)) is non empty set
TopStruct(# the carrier of (X,X0), the topology of (X,X0) #) is non empty strict TopStruct
the topology of (X,A) is Element of bool (bool the carrier of (X,A))
bool the carrier of (X,A) is non empty set
bool (bool the carrier of (X,A)) is non empty set
TopStruct(# the carrier of (X,A), the topology of (X,A) #) is non empty strict TopStruct
(X,A) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A in b₁ ) } is set
union (X,A) is Element of bool the carrier of X
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & X0 in b₁ ) } is set
union (X,X0) is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is set
A is Element of the carrier of X
(X,A) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A in b₁ ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } is set
(Cl {A}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } ) is Element of bool the carrier of X
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty strict TopSpace-like SubSpace of X
(X,X0) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & X0 in b₁ ) } is set
union (X,X0) is Element of bool the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
Cl {X0} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 in b₁ ) } is set
(Cl {X0}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & X0 in b₁ ) } ) is Element of bool the carrier of X
the carrier of (X,X0) is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is non empty TopSpace-like closed SubSpace of X
the carrier of X0 is non empty set
A is Element of the carrier of X
(X,A) is non empty strict TopSpace-like anti-discrete almost_discrete (X) SubSpace of X
bool the carrier of X is non empty set
D is Element of bool the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A in b₁ ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } is set
(Cl {A}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } ) is Element of bool the carrier of X
the carrier of (X,A) is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is non empty TopSpace-like open SubSpace of X
the carrier of X0 is non empty set
A is Element of the carrier of X
(X,A) is non empty strict TopSpace-like anti-discrete almost_discrete (X) SubSpace of X
bool the carrier of X is non empty set
D is Element of bool the carrier of X
(X,A) is non empty Element of bool the carrier of X
(X,A) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & A in b₁ ) } is set
union (X,A) is Element of bool the carrier of X
{A} is non empty trivial V170(X) Element of bool the carrier of X
Cl {A} is non empty closed Element of bool the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } is set
(Cl {A}) /\ (meet { b₁ where b₁ is Element of bool the carrier of X : ( b₁ is open & A in b₁ ) } ) is Element of bool the carrier of X
the carrier of (X,A) is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
{X0} is non empty trivial V170(X) Element of bool the carrier of X
bool the carrier of X is non empty set
Cl {X0} is non empty closed Element of bool the carrier of X
Sspace X0 is non empty trivial V46() V51(1) strict TopSpace-like V160() anti-discrete almost_discrete SubSpace of X
the carrier of (Sspace X0) is non empty trivial V31() set
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
X | X0 is strict SubSpace of X
the carrier of (X | X0) is set
[#] (X | X0) is non proper dense Element of bool the carrier of (X | X0)
bool the carrier of (X | X0) is non empty set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
X | X0 is non empty strict SubSpace of X
the carrier of (X | X0) is non empty set
bool the carrier of (X | X0) is non empty set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is SubSpace of X
the carrier of X0 is set
bool the carrier of X0 is non empty set
A is non empty Element of bool the carrier of X
X | A is non empty strict SubSpace of X
the carrier of (X | A) is non empty set
X is non empty non trivial TopStruct
[#] X is non empty non trivial non proper dense Element of bool the carrier of X
the carrier of X is non empty non trivial set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
X | X0 is non empty strict SubSpace of X
[#] (X | X0) is non empty non proper dense Element of bool the carrier of (X | X0)
the carrier of (X | X0) is non empty set
bool the carrier of (X | X0) is non empty set
X is non empty non trivial TopStruct
the carrier of X is non empty non trivial set
bool the carrier of X is non empty set
X0 is non empty non trivial Element of bool the carrier of X
X | X0 is non empty strict SubSpace of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty non proper Element of bool the carrier of X
X | X0 is non empty strict SubSpace of X
the carrier of (X | X0) is non empty set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is Element of bool the carrier of X
(X,X0) is Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
X | (X,X0) is strict SubSpace of X
the carrier of (X | (X,X0)) is set
[#] (X | (X,X0)) is non proper dense Element of bool the carrier of (X | (X,X0))
bool the carrier of (X | (X,X0)) is non empty set
A is strict SubSpace of X
the carrier of A is set
D is strict SubSpace of X
the carrier of D is set
[#] D is non proper dense Element of bool the carrier of D
bool the carrier of D is non empty set
[#] A is non proper dense Element of bool the carrier of A
bool the carrier of A is non empty set
[#] X is non empty non proper dense Element of bool the carrier of X
A1 is Element of bool the carrier of X
X | A1 is strict SubSpace of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
(X,X0) is strict SubSpace of X
the carrier of (X,X0) is set
(X,X0) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
(X,X0) is non empty strict SubSpace of X
the carrier of (X,X0) is non empty set
bool the carrier of (X,X0) is non empty set
(X,X0) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
X | X0 is non empty strict SubSpace of X
(X,X0) is non empty strict SubSpace of X
the carrier of (X | X0) is non empty set
the carrier of (X,X0) is non empty set
(X,X0) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
X is non empty TopStruct
the carrier of X is non empty set
X0 is Element of the carrier of X
(X,X0) is non empty strict SubSpace of X
the carrier of (X,X0) is non empty set
the topology of (X,X0) is Element of bool (bool the carrier of (X,X0))
bool the carrier of (X,X0) is non empty set
bool (bool the carrier of (X,X0)) is non empty set
TopStruct(# the carrier of (X,X0), the topology of (X,X0) #) is non empty strict TopStruct
{X0} is non empty trivial Element of bool the carrier of X
bool the carrier of X is non empty set
(X,{X0}) is non empty strict SubSpace of X
the carrier of (X,{X0}) is non empty set
the topology of (X,{X0}) is Element of bool (bool the carrier of (X,{X0}))
bool the carrier of (X,{X0}) is non empty set
bool (bool the carrier of (X,{X0})) is non empty set
TopStruct(# the carrier of (X,{X0}), the topology of (X,{X0}) #) is non empty strict TopStruct
(X,{X0}) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in {X0} } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in {X0} } is set
(X,X0) is non empty Element of bool the carrier of X
(X,X0) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ( b₁ is (X) & X0 in b₁ ) } is set
union (X,X0) is Element of bool the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
A is non empty Element of bool the carrier of X
(X,X0) is non empty strict SubSpace of X
(X,A) is non empty strict SubSpace of X
the carrier of (X,A) is non empty set
(X,A) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
the carrier of (X,X0) is non empty set
(X,X0) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
(X,X0) is non empty strict SubSpace of X
the carrier of (X,X0) is non empty set
the topology of (X,X0) is Element of bool (bool the carrier of (X,X0))
bool the carrier of (X,X0) is non empty set
bool (bool the carrier of (X,X0)) is non empty set
TopStruct(# the carrier of (X,X0), the topology of (X,X0) #) is non empty strict TopStruct
(X,X0) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
(X,(X,X0)) is non empty strict SubSpace of X
the carrier of (X,(X,X0)) is non empty set
the topology of (X,(X,X0)) is Element of bool (bool the carrier of (X,(X,X0)))
bool the carrier of (X,(X,X0)) is non empty set
bool (bool the carrier of (X,(X,X0))) is non empty set
TopStruct(# the carrier of (X,(X,X0)), the topology of (X,(X,X0)) #) is non empty strict TopStruct
(X,(X,X0)) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in (X,X0) } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in (X,X0) } is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty Element of bool the carrier of X
A is non empty Element of bool the carrier of X
(X,A) is non empty strict SubSpace of X
the carrier of (X,A) is non empty set
bool the carrier of (X,A) is non empty set
(X,X0) is non empty strict SubSpace of X
(X,A) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
the carrier of (X,X0) is non empty set
(X,X0) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
A is non empty Element of bool the carrier of X
X0 is non empty Element of bool the carrier of X
(X,X0) is non empty strict SubSpace of X
the carrier of (X,X0) is non empty set
bool the carrier of (X,X0) is non empty set
(X,A) is non empty strict SubSpace of X
the carrier of (X,A) is non empty set
bool the carrier of (X,A) is non empty set
the topology of (X,X0) is Element of bool (bool the carrier of (X,X0))
bool (bool the carrier of (X,X0)) is non empty set
TopStruct(# the carrier of (X,X0), the topology of (X,X0) #) is non empty strict TopStruct
the topology of (X,A) is Element of bool (bool the carrier of (X,A))
bool (bool the carrier of (X,A)) is non empty set
TopStruct(# the carrier of (X,A), the topology of (X,A) #) is non empty strict TopStruct
(X,A) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
(X,X0) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
X is non empty non trivial TopStruct
the carrier of X is non empty non trivial set
bool the carrier of X is non empty set
X0 is non empty non trivial Element of bool the carrier of X
(X,X0) is non empty strict SubSpace of X
(X,X0) is non empty non trivial Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
X is non empty TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is non empty non proper Element of bool the carrier of X
(X,X0) is non empty strict SubSpace of X
the carrier of (X,X0) is non empty set
(X,X0) is non empty non proper Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in X0 } is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is TopSpace-like open SubSpace of X
the carrier of X0 is set
bool the carrier of X0 is non empty set
A is non empty Element of bool the carrier of X
(X,A) is non empty strict TopSpace-like SubSpace of X
D is Element of bool the carrier of X
(X,A) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
the carrier of (X,A) is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
X0 is TopSpace-like closed SubSpace of X
the carrier of X0 is set
bool the carrier of X0 is non empty set
A is non empty Element of bool the carrier of X
(X,A) is non empty strict TopSpace-like SubSpace of X
D is Element of bool the carrier of X
(X,A) is non empty Element of bool the carrier of X
{ (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
union { (X,b₁) where b₁ is Element of the carrier of X : b₁ in A } is set
the carrier of (X,A) is non empty set