K87() is set
bool K87() is non empty set
I[01] is TopStruct
the carrier of I[01] is set
{} is empty 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 Element of bool the carrier of X
A is Element of the carrier of X
M is Element of the carrier of X
MaxADSet A is non empty Element of bool the carrier of X
MaxADSet M is non empty Element of bool the carrier of X
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B 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
([#] X) \ B is Element of bool the carrier of X
B ` is Element of bool the carrier of X
the carrier of X \ B is set
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B 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
([#] X) \ B is Element of bool the carrier of X
B ` is Element of bool the carrier of X
the carrier of X \ B is set
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B is Element of bool the carrier of X
A is Element of the carrier of X
M is Element of the carrier of X
MaxADSet A is non empty Element of bool the carrier of X
MaxADSet M is non empty Element of bool the carrier of X
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B is Element of bool the carrier of X
{A} is non empty Element of bool the carrier of X
{M} is non empty Element of bool the carrier of X
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B is Element of bool the carrier of X
{A} is non empty Element of bool the carrier of X
{M} is non empty Element of bool the carrier of X
B is Element of bool the carrier of X
B is Element of bool the carrier of X
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
A is Element of the carrier of X
MaxADSet A is non empty Element of bool the carrier of X
X0 /\ (MaxADSet A) is Element of bool the carrier of X
{A} is non empty Element of bool the carrier of X
M is set
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
A is Element of the carrier of X
M is Element of the carrier of X
MaxADSet A is non empty Element of bool the carrier of X
X0 /\ (MaxADSet A) is Element of bool the carrier of X
{A} is non empty Element of bool the carrier of X
MaxADSet M is non empty Element of bool the carrier of X
X0 /\ (MaxADSet M) is Element of bool the carrier of X
{M} 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 bool the carrier of X
A is Element of the carrier of X
{A} is non empty Element of bool the carrier of X
MaxADSet A is non empty Element of bool the carrier of X
M is non empty Element of bool the carrier of X
X0 /\ M is Element of bool the carrier of X
A is Element of the carrier of X
{A} is non empty Element of bool the carrier of X
M is Element of bool the carrier of X
X0 /\ M is Element of bool the carrier of X
MaxADSet A is non empty Element of bool the carrier of X
X0 /\ (MaxADSet 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
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
M is Element of bool the carrier of X0
B is Element of bool the carrier of X0
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
MaxADSet X0 is Element of bool the carrier of X
A is set
M is Element of the carrier of X
{M} is non empty Element of bool the carrier of X
X0 \/ {M} is non empty Element of bool the carrier of X
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
(X0 \/ {M}) /\ (MaxADSet B) is Element of bool the carrier of X
{B} is non empty Element of bool the carrier of X
{M} /\ (MaxADSet B) is Element of bool the carrier of X
MaxADSet {B} is Element of bool the carrier of X
X0 /\ (MaxADSet B) is Element of bool the carrier of X
(X0 /\ (MaxADSet B)) \/ {} is set
X0 /\ (MaxADSet B) is Element of bool the carrier of X
(MaxADSet B) /\ (MaxADSet X0) is Element of bool the carrier of X
{M} /\ (MaxADSet B) is Element of bool the carrier of X
{} \/ ({M} /\ (MaxADSet B)) is set
A is Element of bool the carrier of X
M is set
B is Element of the carrier of X
{ (MaxADSet b1) where b1 is Element of the carrier of X : b1 in X0 } is set
union { (MaxADSet b1) where b1 is Element of the carrier of X : b1 in X0 } is set
B is set
x is Element of the carrier of X
MaxADSet x is non empty Element of bool the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
X0 /\ (MaxADSet B) is Element of bool the carrier of X
A /\ (MaxADSet B) is Element of bool the carrier of X
{B} is non empty Element of bool the carrier of X
{x} 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 bool the carrier of X
MaxADSet X0 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
Cl (MaxADSet 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
MaxADSet 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 set
M is empty proper open closed boundary nowhere_dense Element of bool the carrier of X
A is Element of the carrier of X
{A} is non empty Element of bool the carrier of X
B is non empty Element of bool the carrier of X
B 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 bool the carrier of X
A is Element of bool the carrier of X
X0 /\ A is Element of bool the carrier of X
MaxADSet (X0 /\ A) is Element of bool the carrier of X
MaxADSet X0 is Element of bool the carrier of X
MaxADSet A is Element of bool the carrier of X
(MaxADSet X0) /\ (MaxADSet A) is Element of bool the carrier of X
(MaxADSet X0) /\ A is Element of bool the carrier of X
the carrier of X /\ A 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 bool the carrier of X
X0 /\ A is Element of bool the carrier of X
MaxADSet (X0 /\ A) is Element of bool the carrier of X
MaxADSet X0 is Element of bool the carrier of X
MaxADSet A is Element of bool the carrier of X
(MaxADSet X0) /\ (MaxADSet A) is Element of bool the carrier of X
(MaxADSet X0) /\ A is Element of bool the carrier of X
the carrier of X /\ A 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 bool the carrier of X
Cl A is closed Element of bool the carrier of X
X0 /\ (Cl A) is Element of bool the carrier of X
MaxADSet (X0 /\ (Cl A)) 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 bool the carrier of X
Int A is open Element of bool the carrier of X
X0 /\ (Int A) is Element of bool the carrier of X
MaxADSet (X0 /\ (Int A)) 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
MaxADSet A is non empty Element of bool the carrier of X
X0 /\ (MaxADSet A) is Element of bool the carrier of X
MaxADSet X0 is Element of bool the carrier of X
{ (MaxADSet b1) where b1 is Element of the carrier of X : b1 in X0 } is set
union { (MaxADSet b1) where b1 is Element of the carrier of X : b1 in X0 } is set
M is set
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
{B} is non empty Element of bool the carrier of X
MaxADSet X0 is Element of bool the carrier of X
A is set
M is Element of the carrier of X
MaxADSet M is non empty Element of bool the carrier of X
X0 /\ (MaxADSet M) is Element of bool the carrier of X
B is Element of the carrier of X
{B} is non empty Element of bool the carrier of X
(MaxADSet M) /\ (MaxADSet X0) is Element of bool the carrier of X
{M} is non empty Element of bool the carrier of X
A is Element of the carrier of X
MaxADSet A is non empty Element of bool the carrier of X
X0 /\ (MaxADSet A) is Element of bool the carrier of X
{A} is non empty Element of bool the carrier of X
M is Element of the carrier of X
{M} 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 bool the carrier of X
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
MaxADSet X0 is Element of bool the carrier of X
([#] X) \ (MaxADSet X0) is Element of bool the carrier of X
{ (MaxADSet b1) where b1 is Element of the carrier of X : b1 in ([#] X) \ (MaxADSet X0) } is set
B is set
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
bool (bool the carrier of X) is non empty set
(MaxADSet X0) ` is Element of bool the carrier of X
the carrier of X \ (MaxADSet X0) is set
X0 /\ (([#] X) \ (MaxADSet X0)) is Element of bool the carrier of X
B is Element of bool (bool the carrier of X)
B is Element of bool (bool the carrier of X)
x is Element of bool the carrier of X
b is Element of the carrier of X
MaxADSet b is non empty Element of bool the carrier of X
{b} is non empty Element of bool the carrier of X
[:B, the carrier of X:] is set
bool [:B, the carrier of X:] is non empty set
x is Relation-like B -defined the carrier of X -valued Function-like V18(B, the carrier of X) Element of bool [:B, the carrier of X:]
x .: B is Element of bool the carrier of X
X0 \/ (x .: B) is Element of bool the carrier of X
a is set
a is set
x . a is set
a is Element of the carrier of X
MaxADSet a is non empty Element of bool the carrier of X
(X0 \/ (x .: B)) /\ (MaxADSet a) is Element of bool the carrier of X
(MaxADSet X0) \/ (([#] X) \ (MaxADSet X0)) is Element of bool the carrier of X
{a} is non empty Element of bool the carrier of X
MaxADSet {a} is Element of bool the carrier of X
(x .: B) /\ (MaxADSet a) is Element of bool the carrier of X
X0 /\ (MaxADSet a) is Element of bool the carrier of X
(X0 /\ (MaxADSet a)) \/ {} is set
{ (MaxADSet b1) where b1 is Element of the carrier of X : b1 in X0 } is set
union { (MaxADSet b1) where b1 is Element of the carrier of X : b1 in X0 } is set
a is set
b is Element of the carrier of X
MaxADSet b is non empty Element of bool the carrier of X
b is Element of the carrier of X
MaxADSet b is non empty Element of bool the carrier of X
{b} is non empty Element of bool the carrier of X
a is Element of the carrier of X
{a} is non empty Element of bool the carrier of X
x . (MaxADSet a) is set
a is Element of the carrier of X
b is set
z is Element of the carrier of X
MaxADSet z is non empty Element of bool the carrier of X
{a} is non empty Element of bool the carrier of X
C is set
x . C is set
C is Element of bool the carrier of X
w is Element of the carrier of X
MaxADSet w is non empty Element of bool the carrier of X
x . (MaxADSet w) is set
b is Element of the carrier of X
{b} is non empty Element of bool the carrier of X
a is Element of the carrier of X
{a} is non empty Element of bool the carrier of X
a is Element of the carrier of X
{a} 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
{} X is empty proper open closed boundary nowhere_dense 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
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
M is Element of bool the carrier of X
X is non empty TopStruct
X0 is SubSpace of X
[#] X0 is non proper dense Element of bool the carrier of X0
the carrier of X0 is set
bool the carrier of X0 is non empty set
[#] X is non empty non proper dense Element of bool the carrier of X
the carrier of X is non empty set
bool the carrier of X is non empty set
X is non empty TopStruct
X0 is non empty 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 SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
the carrier of X0 is non empty set
the topology of X0 is non empty 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
TopStruct(# the carrier of X0, the topology of X0 #) is non empty strict TopSpace-like 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
M is non empty TopSpace-like T_0 SubSpace of X
the carrier of M is non empty set
the topology of M is non empty Element of bool (bool the carrier of M)
bool the carrier of M is non empty set
bool (bool the carrier of M) is non empty set
TopStruct(# the carrier of M, the topology of M #) is non empty strict TopSpace-like TopStruct
B is Element of bool the carrier of X
A is Element of bool the carrier of X
M is Element of bool the carrier of X
B is non empty strict TopSpace-like T_0 SubSpace of X
the carrier of B 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
A is non empty strict TopSpace-like SubSpace of X
the carrier of A is non empty set
X is non empty TopSpace-like TopStruct
X0 is 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 set
A is Element of bool the carrier of X
X0 is TopSpace-like SubSpace of X
X0 is 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 set
A is Element of bool the carrier of X
X0 is TopSpace-like SubSpace of X
X0 is TopSpace-like SubSpace of X
X0 is 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 set
A is Element of bool the carrier of X
X0 is TopSpace-like SubSpace of X
X0 is TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like T_0 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
M is Element of bool the carrier of X
B is non empty strict TopSpace-like SubSpace of X
the carrier of B 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 Element of bool the carrier of X
A is non empty strict TopSpace-like SubSpace of X
the carrier of 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 dense (X) SubSpace of X
the carrier of X0 is set
bool the carrier of X0 is non empty set
A is Element of bool the carrier of X
MaxADSet A is Element of bool the carrier of X
(MaxADSet A) /\ the carrier of X0 is Element of bool the carrier of X
M is Element of bool the carrier of X0
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B /\ B is Element of bool the carrier of X
B is Element of bool the carrier of X
B /\ 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 TopSpace-like dense (X) SubSpace of X
the carrier of X0 is set
bool the carrier of X0 is non empty set
A is Element of bool the carrier of X
MaxADSet A is Element of bool the carrier of X
A /\ the carrier of X0 is Element of bool the carrier of X
M is Element of bool the carrier of X
A /\ M is Element of bool the carrier of X
B is Element of bool the carrier of X0
B is Element of bool the carrier of X0
B is Element of bool the carrier of X0
M is Element of bool the carrier of X
x is Element of bool the carrier of X
MaxADSet x is Element of bool the carrier of X
b is set
a is Element of the carrier of X
MaxADSet a is non empty Element of bool the carrier of X
M /\ (MaxADSet a) is Element of bool the carrier of X
a is Element of the carrier of X
{a} is non empty Element of bool the carrier of X
{a} is non empty Element of bool the carrier of X
MaxADSet {a} is Element of bool the carrier of X
MaxADSet {a} is Element of bool the carrier of X
MaxADSet a 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 TopSpace-like dense (X) SubSpace of X
the carrier of X0 is set
bool the carrier of X0 is non empty set
M is Element of bool the carrier of X
MaxADSet M is Element of bool the carrier of X
(MaxADSet M) /\ the carrier of X0 is Element of bool the carrier of X
B is Element of bool the carrier of X0
A is Element of bool the carrier of X
B is Element of bool the carrier of X
B /\ A is Element of bool the carrier of X
B is Element of bool the carrier of X
B /\ A 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 TopSpace-like dense (X) SubSpace of X
the carrier of X0 is set
bool the carrier of X0 is non empty set
M is Element of bool the carrier of X
MaxADSet M is Element of bool the carrier of X
M /\ the carrier of X0 is Element of bool the carrier of X
A is Element of bool the carrier of X
M /\ A is Element of bool the carrier of X
B is Element of bool the carrier of X0
B is Element of bool the carrier of X0
A is Element of bool the carrier of X
x is Element of bool the carrier of X
MaxADSet x is Element of bool the carrier of X
b is set
a is Element of the carrier of X
MaxADSet a is non empty Element of bool the carrier of X
A /\ (MaxADSet a) is Element of bool the carrier of X
a is Element of the carrier of X
{a} is non empty Element of bool the carrier of X
{a} is non empty Element of bool the carrier of X
MaxADSet {a} is Element of bool the carrier of X
MaxADSet {a} is Element of bool the carrier of X
MaxADSet a 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) Element of bool [: the carrier of X, the carrier of X0:]
M is Element of bool the carrier of X
B is Element of bool the carrier of X
bool the carrier of X0 is non empty set
B is Element of bool the carrier of X0
A " B is Element of bool the carrier of X
x is Element of bool the carrier of X
{ (MaxADSet b1) where b1 is Element of the carrier of X : b1 in x } is set
a is set
a is Element of the carrier of X
A . a is Element of the carrier of X0
b is Element of the carrier of X
MaxADSet b is non empty Element of bool the carrier of X
union { (MaxADSet b1) where b1 is Element of the carrier of X : b1 in x } is set
MaxADSet a is non empty Element of bool the carrier of X
M /\ (MaxADSet a) is Element of bool the carrier of X
{b} is non empty Element of bool the carrier of X
{a} is non empty Element of bool the carrier of X
[#] X0 is non empty non proper open closed dense non boundary Element of bool the carrier of X0
MaxADSet x is 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 X0
a is set
a is Element of the carrier of X
MaxADSet a is non empty Element of bool the carrier of X
b is set
b is Element of the carrier of X
MaxADSet b is non empty Element of bool the carrier of X
M /\ (MaxADSet b) is Element of bool the carrier of X
A . b is Element of the carrier of X0
{(A . b)} is non empty Element of bool the carrier of X0
M /\ (MaxADSet a) is Element of bool the carrier of X
{a} is non empty Element of bool the carrier of X
A . b is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) Element of bool [: the carrier of X, the carrier of X0:]
bool the carrier of X is non empty set
M is Element of bool the carrier of X
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
M /\ (MaxADSet B) is Element of bool the carrier of X
A . B is Element of the carrier of X0
{(A . B)} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
M /\ (MaxADSet B) is Element of bool the carrier of X
{B} 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
M is Element of bool the carrier of X
B is Element of bool the carrier of X
B is Element of the carrier of X
A . B is Element of the carrier of X0
MaxADSet B is non empty Element of bool the carrier of X
M /\ (MaxADSet B) is Element of bool the carrier of X
{B} is non empty Element of bool the carrier of X
{(A . B)} is non empty Element of bool the carrier of X0
bool the carrier of 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 T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
bool the carrier of X is non empty set
M is Element of bool the carrier of X
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
M /\ (MaxADSet B) is Element of bool the carrier of X
A . B is Element of the carrier of X0
{(A . B)} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
M /\ (MaxADSet B) is Element of bool the carrier of X
{B} 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
X0 is non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
bool the carrier of X is non empty set
A is Element of bool the carrier of X
M is Element of the carrier of X
MaxADSet M is non empty Element of bool the carrier of X
A /\ (MaxADSet M) is Element of bool the carrier of X
B is Element of the carrier of X
{B} is non empty Element of bool the carrier of X
B is Element of the carrier of X0
{B} is non empty set
M is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) Element of bool [: the carrier of X, the carrier of X0:]
B is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X is non empty set
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
bool the carrier of X is non empty set
B is Element of the carrier of X
{B} is non empty Element of bool the carrier of X
Cl {B} is closed Element of bool the carrier of X
B is Element of the carrier of X0
{B} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
Cl {B} is closed Element of bool the carrier of X0
A " (Cl {B}) is Element of bool the carrier of X
A . B is Element of the carrier of X0
A " {B} is Element of bool the carrier of X
M is Element of bool the carrier of X
x is set
b is Element of the carrier of X
MaxADSet b is non empty Element of bool the carrier of X
M /\ (MaxADSet b) is Element of bool the carrier of X
a is Element of the carrier of X
{a} is non empty Element of bool the carrier of X
{b} is non empty Element of bool the carrier of X
A . a is Element of the carrier of X0
a is Element of the carrier of X0
MaxADSet a 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
M is Element of bool the carrier of X
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
M /\ (MaxADSet B) is Element of bool the carrier of X
A . B is Element of the carrier of X0
{(A . B)} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
B is Element of bool the carrier of X
x is Element of the carrier of X
{x} is non empty Element of bool the carrier of X
MaxADSet x is non empty Element of bool the carrier of X
Cl {(A . B)} is closed Element of bool the carrier of X0
{B} is non empty Element of bool the carrier of X
a is Element of the carrier of X0
{a} is non empty Element of bool the carrier of X0
Cl {a} is closed Element of bool the carrier of X0
A " (Cl {a}) is Element of bool the carrier of X
Cl {x} is closed Element of bool the carrier of X
A " (Cl {(A . B)}) is Element of bool the carrier of X
b is Element of the carrier of X
{b} is non empty Element of bool the carrier of X
Cl {b} is closed Element of bool the carrier of X
MaxADSet b 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
X0 is non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
bool the carrier of X is non empty set
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
B is Element of the carrier of X0
{B} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
A " {B} is Element of bool the carrier of X
x is set
b is Element of the carrier of X
MaxADSet b is non empty Element of bool the carrier of X
{b} is non empty Element of bool the carrier of X
Cl {B} is closed Element of bool the carrier of X0
A " (Cl {B}) is Element of bool the carrier of X
{B} is non empty Element of bool the carrier of X
Cl {B} is closed Element of bool the carrier of X
A . b is Element of the carrier of X0
M is Element of bool the carrier of X
{(A . b)} is non empty Element of bool the carrier of X0
Cl {(A . b)} is closed Element of bool the carrier of X0
A " (Cl {(A . b)}) is Element of bool the carrier of X
a is Element of the carrier of X
{a} is non empty Element of bool the carrier of X
Cl {a} is closed Element of bool the carrier of X
MaxADSet a is non empty Element of bool the carrier of X
A . B is Element of the carrier of X0
M /\ (MaxADSet B) 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
bool the carrier of X is non empty set
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
B is Element of the carrier of X0
{B} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
A " {B} is Element of bool the carrier of X
x is set
b is Element of the carrier of X
A . b is Element of the carrier of X0
{(A . b)} is non empty Element of bool the carrier of X0
M is Element of bool the carrier of X
MaxADSet b is non empty Element of bool the carrier of X
M /\ (MaxADSet b) is Element of bool the carrier of X
{B} is non empty Element of bool the carrier of X
{b} 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
bool the carrier of X0 is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
B is Element of bool the carrier of X
MaxADSet B is Element of bool the carrier of X
B is Element of bool the carrier of X0
A " B is Element of bool the carrier of X
{ (MaxADSet b1) where b1 is Element of the carrier of X : b1 in B } is set
b is set
a is Element of the carrier of X
A . a is Element of the carrier of X0
a is Element of the carrier of X
MaxADSet a is non empty Element of bool the carrier of X
union { (MaxADSet b1) where b1 is Element of the carrier of X : b1 in B } is set
M is Element of bool the carrier of X
MaxADSet a is non empty Element of bool the carrier of X
M /\ (MaxADSet a) is Element of bool the carrier of X
{a} is non empty Element of bool the carrier of X
{a} is non empty Element of bool the carrier of X
b is set
a is Element of the carrier of X
MaxADSet a is non empty Element of bool the carrier of X
a is set
b is Element of the carrier of X
MaxADSet b is non empty Element of bool the carrier of X
M /\ (MaxADSet b) is Element of bool the carrier of X
A . b is Element of the carrier of X0
{(A . b)} is non empty Element of bool the carrier of X0
M /\ (MaxADSet a) is Element of bool the carrier of X
{a} is non empty Element of bool the carrier of X
A . a is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
bool the carrier of X is non empty set
M is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
B is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
B is set
M . B is set
B . B is set
A is non empty Element of bool the carrier of X
x is Element of the carrier of X
MaxADSet x is non empty Element of bool the carrier of X
A /\ (MaxADSet x) is Element of bool the carrier of X
B . x is Element of the carrier of X0
{(B . x)} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
M . x is Element of the carrier of X0
{(M . x)} is non empty Element of bool the carrier of X0
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Element of the carrier of X
{A} is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
Cl {A} is closed Element of bool the carrier of X
M is Element of the carrier of X0
{M} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
Cl {M} is closed Element of bool the carrier of X0
(X,X0) " (Cl {M}) 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Element of the carrier of X
MaxADSet A is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
M is Element of the carrier of X0
{M} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
(X,X0) " {M} 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
bool the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Element of bool the carrier of X
MaxADSet A is Element of bool the carrier of X
M is Element of bool the carrier of X0
(X,X0) " M 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
bool the carrier of X is non empty set
M is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
B is Element of bool the carrier of X
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
B /\ (MaxADSet B) is Element of bool the carrier of X
M . B is Element of the carrier of X0
{(M . B)} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
A is Element of bool the carrier of X
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
A /\ (MaxADSet B) is Element of bool the carrier of X
M . B is Element of the carrier of X0
{(M . B)} is non empty Element of bool the carrier of X0
bool the carrier of 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 T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
bool the carrier of X is non empty set
M is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
B is Element of the carrier of X
M . B is Element of the carrier of X0
MaxADSet B is non empty Element of bool the carrier of X
A is Element of bool the carrier of X
A /\ (MaxADSet B) is Element of bool the carrier of X
{(M . B)} is non empty Element of bool the carrier of X0
bool the carrier of 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 T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Element of the carrier of X
(X,X0) . A is Element of the carrier of X0
{((X,X0) . A)} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
(X,X0) " {((X,X0) . A)} is Element of bool the carrier of X
bool the carrier of X is non empty set
MaxADSet A is non empty Element of bool the carrier of X
M is Element of bool the carrier of X
B is Element of the carrier of X
MaxADSet B 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
X0 is non empty TopSpace-like T_0 dense (X) SubSpace of X
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Element of the carrier of X
Im ((X,X0),A) is set
{A} is non empty set
(X,X0) .: {A} is set
MaxADSet A is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
(X,X0) .: (MaxADSet A) is Element of bool the carrier of X0
bool the carrier of X0 is non empty set
dom (X,X0) 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
(X,X0) . A is Element of the carrier of X0
{((X,X0) . A)} is non empty Element of bool the carrier of X0
(X,X0) " {((X,X0) . A)} is Element of bool the carrier of X
(X,X0) .: ((X,X0) " {((X,X0) . A)}) is Element of bool the carrier of X0
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
X0 is non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
bool the carrier of X is non empty set
A is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
M is Element of bool the carrier of X
B is Element of bool the carrier of X
MaxADSet B is Element of bool the carrier of X
M /\ (MaxADSet B) is Element of bool the carrier of X
A .: B is Element of bool the carrier of X0
bool the carrier of X0 is non empty set
B is Element of bool the carrier of X
x is set
b is Element of the carrier of X
MaxADSet b is non empty Element of bool the carrier of X
M /\ (MaxADSet b) is Element of bool the carrier of X
{b} is non empty Element of bool the carrier of X
{ (MaxADSet b1) where b1 is Element of the carrier of X : b1 in B } is set
union { (MaxADSet b1) where b1 is Element of the carrier of X : b1 in B } is set
a is set
a is Element of the carrier of X
MaxADSet a is non empty Element of bool the carrier of X
A . a is Element of the carrier of X0
{(A . a)} is non empty Element of bool the carrier of X0
x is set
b is Element of the carrier of X0
a is set
A . a is set
a is Element of the carrier of X
{a} is non empty Element of bool the carrier of X
MaxADSet {a} is Element of bool the carrier of X
MaxADSet a is non empty Element of bool the carrier of X
M /\ (MaxADSet a) is Element of bool the carrier of X
{b} is non empty Element of bool the carrier of X0
dom A 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
M is Element of bool the carrier of X
B is Element of the carrier of X
MaxADSet B is non empty Element of bool the carrier of X
M /\ (MaxADSet B) is Element of bool the carrier of X
A . B is Element of the carrier of X0
{(A . B)} is non empty Element of bool the carrier of X0
bool the carrier of X0 is non empty set
{B} is non empty Element of bool the carrier of X
MaxADSet {B} is Element of bool the carrier of X
M /\ (MaxADSet {B}) is Element of bool the carrier of X
Im (A,B) is set
{B} is non empty set
A .: {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 TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Element of bool the carrier of X
(X,X0) .: A is Element of bool the carrier of X0
bool the carrier of X0 is non empty set
(X,X0) " ((X,X0) .: A) is Element of bool the carrier of X
MaxADSet A is Element of bool the carrier of X
M is non empty Element of bool the carrier of X
M /\ (MaxADSet A) is Element of bool the carrier of X
B is Element of bool the carrier of X
MaxADSet 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Element of bool the carrier of X
(X,X0) .: A is Element of bool the carrier of X0
bool the carrier of X0 is non empty set
MaxADSet A is Element of bool the carrier of X
(X,X0) .: (MaxADSet A) is Element of bool the carrier of X0
rng (X,X0) is Element of bool the carrier of X0
(X,X0) .: the carrier of X is Element of bool the carrier of X0
(X,X0) " ((X,X0) .: A) is Element of bool the carrier of X
(X,X0) .: ((X,X0) " ((X,X0) .: A)) is Element of bool the carrier of X0
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 T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B \/ B is Element of bool the carrier of X
(X,X0) .: (B \/ B) is Element of bool the carrier of X0
bool the carrier of X0 is non empty set
(X,X0) .: B is Element of bool the carrier of X0
(X,X0) .: B is Element of bool the carrier of X0
((X,X0) .: B) \/ ((X,X0) .: B) is Element of bool the carrier of X0
A is Element of bool the carrier of X
MaxADSet (B \/ B) is Element of bool the carrier of X
A /\ (MaxADSet (B \/ B)) is Element of bool the carrier of X
MaxADSet B is Element of bool the carrier of X
MaxADSet B is Element of bool the carrier of X
(MaxADSet B) \/ (MaxADSet B) is Element of bool the carrier of X
A /\ ((MaxADSet B) \/ (MaxADSet B)) is Element of bool the carrier of X
A /\ (MaxADSet B) is Element of bool the carrier of X
A /\ (MaxADSet B) is Element of bool the carrier of X
(A /\ (MaxADSet B)) \/ (A /\ (MaxADSet B)) is Element of bool the carrier of X
((X,X0) .: B) \/ (A /\ (MaxADSet 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 TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B /\ B is Element of bool the carrier of X
(X,X0) .: (B /\ B) is Element of bool the carrier of X0
bool the carrier of X0 is non empty set
(X,X0) .: B is Element of bool the carrier of X0
(X,X0) .: B is Element of bool the carrier of X0
((X,X0) .: B) /\ ((X,X0) .: B) is Element of bool the carrier of X0
A is Element of bool the carrier of X
MaxADSet (B /\ B) is Element of bool the carrier of X
A /\ (MaxADSet (B /\ B)) is Element of bool the carrier of X
A /\ A is Element of bool the carrier of X
MaxADSet B is Element of bool the carrier of X
MaxADSet B is Element of bool the carrier of X
(MaxADSet B) /\ (MaxADSet B) is Element of bool the carrier of X
(A /\ A) /\ ((MaxADSet B) /\ (MaxADSet B)) is Element of bool the carrier of X
A /\ ((MaxADSet B) /\ (MaxADSet B)) is Element of bool the carrier of X
A /\ (A /\ ((MaxADSet B) /\ (MaxADSet B))) is Element of bool the carrier of X
A /\ (MaxADSet B) is Element of bool the carrier of X
(A /\ (MaxADSet B)) /\ (MaxADSet B) is Element of bool the carrier of X
((A /\ (MaxADSet B)) /\ (MaxADSet B)) /\ A is Element of bool the carrier of X
A /\ (MaxADSet B) is Element of bool the carrier of X
(A /\ (MaxADSet B)) /\ (A /\ (MaxADSet B)) is Element of bool the carrier of X
((X,X0) .: B) /\ (A /\ (MaxADSet 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
B is Element of bool the carrier of X
B is Element of bool the carrier of X
B /\ B is Element of bool the carrier of X
(X,X0) .: (B /\ B) is Element of bool the carrier of X0
bool the carrier of X0 is non empty set
(X,X0) .: B is Element of bool the carrier of X0
(X,X0) .: B is Element of bool the carrier of X0
((X,X0) .: B) /\ ((X,X0) .: B) is Element of bool the carrier of X0
A is Element of bool the carrier of X
MaxADSet (B /\ B) is Element of bool the carrier of X
A /\ (MaxADSet (B /\ B)) is Element of bool the carrier of X
A /\ A is Element of bool the carrier of X
MaxADSet B is Element of bool the carrier of X
MaxADSet B is Element of bool the carrier of X
(MaxADSet B) /\ (MaxADSet B) is Element of bool the carrier of X
(A /\ A) /\ ((MaxADSet B) /\ (MaxADSet B)) is Element of bool the carrier of X
A /\ ((MaxADSet B) /\ (MaxADSet B)) is Element of bool the carrier of X
A /\ (A /\ ((MaxADSet B) /\ (MaxADSet B))) is Element of bool the carrier of X
A /\ (MaxADSet B) is Element of bool the carrier of X
(A /\ (MaxADSet B)) /\ (MaxADSet B) is Element of bool the carrier of X
((A /\ (MaxADSet B)) /\ (MaxADSet B)) /\ A is Element of bool the carrier of X
A /\ (MaxADSet B) is Element of bool the carrier of X
(A /\ (MaxADSet B)) /\ (A /\ (MaxADSet B)) is Element of bool the carrier of X
((X,X0) .: B) /\ (A /\ (MaxADSet 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Element of bool the carrier of X
(X,X0) .: A is Element of bool the carrier of X0
bool the carrier of X0 is non empty set
MaxADSet A is Element of bool the carrier of X
M is Element of bool the carrier of X
A /\ M 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 non empty TopSpace-like T_0 dense (X) SubSpace of X
the carrier of X0 is non empty set
(X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V18( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
A is Element of bool the carrier of X
(X,X0) .: A is Element of bool the carrier of X0
bool the carrier of X0 is non empty set
MaxADSet A is Element of bool the carrier of X
M is Element of bool the carrier of X
A /\ M is Element of bool the carrier of X