:: TSP_2 semantic presentation

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 b

union { (MaxADSet b

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 b

union { (MaxADSet b

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 b

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 b

union { (MaxADSet b

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 b

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 b

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 b

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 b

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 b

union { (MaxADSet b

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