:: BORSUK_3 semantic presentation

{} is empty trivial set

the empty trivial set is empty trivial set

1 is non empty set

{{},1} is non empty set

K103() is set

bool K103() is non empty set

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 compact TopStruct

the carrier of I[01] is non empty set

T1 is TopSpace-like TopStruct

T2 is TopSpace-like TopStruct

[:T1,T2:] is strict TopSpace-like TopStruct

[#] [:T1,T2:] is non proper open closed dense Element of bool the carrier of [:T1,T2:]

the carrier of [:T1,T2:] is set

bool the carrier of [:T1,T2:] is non empty set

[#] T1 is non proper open closed dense Element of bool the carrier of T1

the carrier of T1 is set

bool the carrier of T1 is non empty set

[#] T2 is non proper open closed dense Element of bool the carrier of T2

the carrier of T2 is set

bool the carrier of T2 is non empty set

[:([#] T1),([#] T2):] is Element of bool the carrier of [:T1,T2:]

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

T2 is non empty TopSpace-like TopStruct

the carrier of T2 is non empty set

S1 is Element of the carrier of T1

T2 --> S1 is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of T1:]

[: the carrier of T2, the carrier of T1:] is non empty set

bool [: the carrier of T2, the carrier of T1:] is non empty set

the carrier of T2 --> S1 is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of T1:]

{S1} is non empty trivial compact Element of bool the carrier of T1

bool the carrier of T1 is non empty set

T1 | {S1} is non empty strict TopSpace-like SubSpace of T1

the carrier of (T1 | {S1}) is non empty set

[: the carrier of T2, the carrier of (T1 | {S1}):] is non empty set

bool [: the carrier of T2, the carrier of (T1 | {S1}):] is non empty set

T2 is Relation-like the carrier of T2 -defined the carrier of (T1 | {S1}) -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of (T1 | {S1}):]

T1 is TopStruct

id T1 is Relation-like the carrier of T1 -defined the carrier of T1 -valued Function-like total quasi_total continuous open Element of bool [: the carrier of T1, the carrier of T1:]

the carrier of T1 is set

[: the carrier of T1, the carrier of T1:] is set

bool [: the carrier of T1, the carrier of T1:] is non empty set

id the carrier of T1 is Relation-like the carrier of T1 -defined the carrier of T1 -valued total quasi_total Element of bool [: the carrier of T1, the carrier of T1:]

T1 is TopStruct

id T1 is Relation-like the carrier of T1 -defined the carrier of T1 -valued Function-like total quasi_total continuous being_homeomorphism open Element of bool [: the carrier of T1, the carrier of T1:]

the carrier of T1 is set

[: the carrier of T1, the carrier of T1:] is set

bool [: the carrier of T1, the carrier of T1:] is non empty set

id the carrier of T1 is Relation-like the carrier of T1 -defined the carrier of T1 -valued total quasi_total Element of bool [: the carrier of T1, the carrier of T1:]

T1 is non empty TopStruct

T2 is non empty TopStruct

the carrier of T1 is non empty set

the carrier of T2 is non empty set

[: the carrier of T1, the carrier of T2:] is non empty set

bool [: the carrier of T1, the carrier of T2:] is non empty set

S1 is Relation-like the carrier of T1 -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T1, the carrier of T2:]

S1 " is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of T1:]

[: the carrier of T2, the carrier of T1:] is non empty set

bool [: the carrier of T2, the carrier of T1:] is non empty set

S1 is TopStruct

S1 is non empty TopStruct

S1 is non empty TopStruct

S2 is non empty TopStruct

T1 is non empty TopSpace-like TopStruct

T2 is non empty TopSpace-like TopStruct

S1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

the carrier of T2 is non empty set

[: the carrier of T1, the carrier of T2:] is non empty set

bool [: the carrier of T1, the carrier of T2:] is non empty set

S2 is Relation-like the carrier of T1 -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T1, the carrier of T2:]

the carrier of S1 is non empty set

[: the carrier of T2, the carrier of S1:] is non empty set

bool [: the carrier of T2, the carrier of S1:] is non empty set

S2 is Relation-like the carrier of T2 -defined the carrier of S1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of S1:]

S2 * S2 is Relation-like the carrier of T1 -defined the carrier of S1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T1, the carrier of S1:]

[: the carrier of T1, the carrier of S1:] is non empty set

bool [: the carrier of T1, the carrier of S1:] is non empty set

T1 is TopStruct

the carrier of T1 is set

bool the carrier of T1 is non empty set

T2 is empty trivial boundary compact Element of bool the carrier of T1

T1 | T2 is empty trivial finite V48( {} ) strict T_0 T_1 T_2 SubSpace of T1

T1 is TopSpace-like TopStruct

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

T2 is non empty TopSpace-like TopStruct

the carrier of T2 is non empty set

S1 is Element of the carrier of T1

{S1} is non empty trivial compact Element of bool the carrier of T1

bool the carrier of T1 is non empty set

T1 | {S1} is non empty strict TopSpace-like SubSpace of T1

[:T2,(T1 | {S1}):] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,(T1 | {S1}):] is non empty set

[: the carrier of [:T2,(T1 | {S1}):], the carrier of T2:] is non empty set

bool [: the carrier of [:T2,(T1 | {S1}):], the carrier of T2:] is non empty set

[: the carrier of T2,{S1}:] is non empty set

pr1 ( the carrier of T2,{S1}) is Relation-like [: the carrier of T2,{S1}:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T2,{S1}:], the carrier of T2:]

[:[: the carrier of T2,{S1}:], the carrier of T2:] is non empty set

bool [:[: the carrier of T2,{S1}:], the carrier of T2:] is non empty set

S2 is Relation-like the carrier of [:T2,(T1 | {S1}):] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:T2,(T1 | {S1}):], the carrier of T2:]

T2 is set

dom S2 is set

S2 is set

S2 . T2 is set

S2 . S2 is set

dom S2 is Element of bool the carrier of [:T2,(T1 | {S1}):]

bool the carrier of [:T2,(T1 | {S1}):] is non empty set

S1 is set

X is set

[S1,X] is non empty set

{S1,X} is non empty set

{S1} is non empty trivial set

{{S1,X},{S1}} is non empty set

Q9 is set

A is set

[Q9,A] is non empty set

{Q9,A} is non empty set

{Q9} is non empty trivial set

{{Q9,A},{Q9}} is non empty set

S2 . (S1,X) is set

S2 . [S1,X] is set

S2 . (Q9,A) is set

S2 . [Q9,A] is set

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

T2 is non empty TopSpace-like TopStruct

the carrier of T2 is non empty set

S1 is Element of the carrier of T1

{S1} is non empty trivial compact Element of bool the carrier of T1

bool the carrier of T1 is non empty set

T1 | {S1} is non empty strict TopSpace-like SubSpace of T1

[:(T1 | {S1}),T2:] is non empty strict TopSpace-like TopStruct

the carrier of [:(T1 | {S1}),T2:] is non empty set

[: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:] is non empty set

bool [: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:] is non empty set

[:{S1}, the carrier of T2:] is non empty set

pr2 ({S1}, the carrier of T2) is Relation-like [:{S1}, the carrier of T2:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [:[:{S1}, the carrier of T2:], the carrier of T2:]

[:[:{S1}, the carrier of T2:], the carrier of T2:] is non empty set

bool [:[:{S1}, the carrier of T2:], the carrier of T2:] is non empty set

S2 is Relation-like the carrier of [:(T1 | {S1}),T2:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:]

T2 is set

dom S2 is set

S2 is set

S2 . T2 is set

S2 . S2 is set

dom S2 is Element of bool the carrier of [:(T1 | {S1}),T2:]

bool the carrier of [:(T1 | {S1}),T2:] is non empty set

S1 is set

X is set

[S1,X] is non empty set

{S1,X} is non empty set

{S1} is non empty trivial set

{{S1,X},{S1}} is non empty set

Q9 is set

A is set

[Q9,A] is non empty set

{Q9,A} is non empty set

{Q9} is non empty trivial set

{{Q9,A},{Q9}} is non empty set

S2 . (S1,X) is set

S2 . [S1,X] is set

S2 . (Q9,A) is set

S2 . [Q9,A] is set

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

T2 is non empty TopSpace-like TopStruct

the carrier of T2 is non empty set

[: the carrier of T2, the carrier of T1:] is non empty set

id T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued Function-like non empty total quasi_total continuous being_homeomorphism open Element of bool [: the carrier of T2, the carrier of T2:]

[: the carrier of T2, the carrier of T2:] is non empty set

bool [: the carrier of T2, the carrier of T2:] is non empty set

id the carrier of T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued non empty total quasi_total Element of bool [: the carrier of T2, the carrier of T2:]

S1 is Element of the carrier of T1

{S1} is non empty trivial compact Element of bool the carrier of T1

bool the carrier of T1 is non empty set

T1 | {S1} is non empty strict TopSpace-like SubSpace of T1

[:T2,(T1 | {S1}):] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,(T1 | {S1}):] is non empty set

[: the carrier of [:T2,(T1 | {S1}):], the carrier of T2:] is non empty set

bool [: the carrier of [:T2,(T1 | {S1}):], the carrier of T2:] is non empty set

[: the carrier of T2,{S1}:] is non empty set

pr1 ( the carrier of T2,{S1}) is Relation-like [: the carrier of T2,{S1}:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T2,{S1}:], the carrier of T2:]

[:[: the carrier of T2,{S1}:], the carrier of T2:] is non empty set

bool [:[: the carrier of T2,{S1}:], the carrier of T2:] is non empty set

T2 --> S1 is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of T1:]

bool [: the carrier of T2, the carrier of T1:] is non empty set

the carrier of T2 --> S1 is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of T1:]

<:(id T2),(T2 --> S1):> is Relation-like the carrier of T2 -defined [: the carrier of T2, the carrier of T1:] -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2,[: the carrier of T2, the carrier of T1:]:]

[: the carrier of T2,[: the carrier of T2, the carrier of T1:]:] is non empty set

bool [: the carrier of T2,[: the carrier of T2, the carrier of T1:]:] is non empty set

S2 is Relation-like the carrier of [:T2,(T1 | {S1}):] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:T2,(T1 | {S1}):], the carrier of T2:]

S2 " is Relation-like the carrier of T2 -defined the carrier of [:T2,(T1 | {S1}):] -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of [:T2,(T1 | {S1}):]:]

[: the carrier of T2, the carrier of [:T2,(T1 | {S1}):]:] is non empty set

bool [: the carrier of T2, the carrier of [:T2,(T1 | {S1}):]:] is non empty set

rng (id T2) is Element of bool the carrier of T2

bool the carrier of T2 is non empty set

rng S2 is Element of bool the carrier of T2

S2 is non empty Element of bool the carrier of T1

T1 | S2 is non empty strict TopSpace-like SubSpace of T1

the carrier of (T1 | S2) is non empty set

[: the carrier of T2, the carrier of (T1 | S2):] is non empty set

bool [: the carrier of T2, the carrier of (T1 | S2):] is non empty set

[:T2,(T1 | S2):] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,(T1 | S2):] is non empty set

[: the carrier of T2, the carrier of [:T2,(T1 | S2):]:] is non empty set

bool [: the carrier of T2, the carrier of [:T2,(T1 | S2):]:] is non empty set

S1 is Relation-like the carrier of T2 -defined the carrier of (T1 | S2) -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of (T1 | S2):]

<:(id T2),S1:> is Relation-like the carrier of T2 -defined [: the carrier of T2, the carrier of (T1 | S2):] -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2,[: the carrier of T2, the carrier of (T1 | S2):]:]

[: the carrier of T2,[: the carrier of T2, the carrier of (T1 | S2):]:] is non empty set

bool [: the carrier of T2,[: the carrier of T2, the carrier of (T1 | S2):]:] is non empty set

[: the carrier of T2,S2:] is non empty set

X is Relation-like the carrier of T2 -defined the carrier of [:T2,(T1 | S2):] -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of [:T2,(T1 | S2):]:]

rng X is Element of bool the carrier of [:T2,(T1 | S2):]

bool the carrier of [:T2,(T1 | S2):] is non empty set

Q9 is set

A is set

A is set

[A,A] is non empty set

{A,A} is non empty set

{A} is non empty trivial set

{{A,A},{A}} is non empty set

[A,S1] is non empty set

{A,S1} is non empty set

{{A,S1},{A}} is non empty set

S1 . A is set

( the carrier of T2 --> S1) . A is set

dom X is Element of bool the carrier of T2

X . A is set

(id T2) . A is set

[((id T2) . A),(S1 . A)] is non empty set

{((id T2) . A),(S1 . A)} is non empty set

{((id T2) . A)} is non empty trivial set

{{((id T2) . A),(S1 . A)},{((id T2) . A)}} is non empty set

rng S1 is Element of bool the carrier of (T1 | S2)

bool the carrier of (T1 | S2) is non empty set

[:(rng (id T2)),(rng S1):] is Element of bool the carrier of [:T2,(T1 | S2):]

dom S2 is Element of bool the carrier of [:T2,(T1 | {S1}):]

bool the carrier of [:T2,(T1 | {S1}):] is non empty set

dom S1 is Element of bool the carrier of T2

dom (id T2) is Element of bool the carrier of T2

S2 * X is Relation-like the carrier of T2 -defined the carrier of T2 -valued Function-like Element of bool [: the carrier of T2, the carrier of T2:]

id (rng S2) is Relation-like rng S2 -defined rng S2 -valued total quasi_total Element of bool [:(rng S2),(rng S2):]

[:(rng S2),(rng S2):] is set

bool [:(rng S2),(rng S2):] is non empty set

S2 " is Relation-like Function-like set

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

T2 is non empty TopSpace-like TopStruct

the carrier of T2 is non empty set

[: the carrier of T1, the carrier of T2:] is non empty set

id T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued Function-like non empty total quasi_total continuous being_homeomorphism open Element of bool [: the carrier of T2, the carrier of T2:]

[: the carrier of T2, the carrier of T2:] is non empty set

bool [: the carrier of T2, the carrier of T2:] is non empty set

id the carrier of T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued non empty total quasi_total Element of bool [: the carrier of T2, the carrier of T2:]

S1 is Element of the carrier of T1

{S1} is non empty trivial compact Element of bool the carrier of T1

bool the carrier of T1 is non empty set

T1 | {S1} is non empty strict TopSpace-like SubSpace of T1

[:(T1 | {S1}),T2:] is non empty strict TopSpace-like TopStruct

the carrier of [:(T1 | {S1}),T2:] is non empty set

[: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:] is non empty set

bool [: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:] is non empty set

[:{S1}, the carrier of T2:] is non empty set

pr2 ({S1}, the carrier of T2) is Relation-like [:{S1}, the carrier of T2:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [:[:{S1}, the carrier of T2:], the carrier of T2:]

[:[:{S1}, the carrier of T2:], the carrier of T2:] is non empty set

bool [:[:{S1}, the carrier of T2:], the carrier of T2:] is non empty set

T2 --> S1 is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of T1:]

[: the carrier of T2, the carrier of T1:] is non empty set

bool [: the carrier of T2, the carrier of T1:] is non empty set

the carrier of T2 --> S1 is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of T1:]

<:(T2 --> S1),(id T2):> is Relation-like the carrier of T2 -defined [: the carrier of T1, the carrier of T2:] -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2,[: the carrier of T1, the carrier of T2:]:]

[: the carrier of T2,[: the carrier of T1, the carrier of T2:]:] is non empty set

bool [: the carrier of T2,[: the carrier of T1, the carrier of T2:]:] is non empty set

S2 is Relation-like the carrier of [:(T1 | {S1}),T2:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:]

S2 " is Relation-like the carrier of T2 -defined the carrier of [:(T1 | {S1}),T2:] -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of [:(T1 | {S1}),T2:]:]

[: the carrier of T2, the carrier of [:(T1 | {S1}),T2:]:] is non empty set

bool [: the carrier of T2, the carrier of [:(T1 | {S1}),T2:]:] is non empty set

rng (id T2) is Element of bool the carrier of T2

bool the carrier of T2 is non empty set

rng S2 is Element of bool the carrier of T2

S2 is non empty Element of bool the carrier of T1

T1 | S2 is non empty strict TopSpace-like SubSpace of T1

the carrier of (T1 | S2) is non empty set

[: the carrier of T2, the carrier of (T1 | S2):] is non empty set

bool [: the carrier of T2, the carrier of (T1 | S2):] is non empty set

[:(T1 | S2),T2:] is non empty strict TopSpace-like TopStruct

the carrier of [:(T1 | S2),T2:] is non empty set

[: the carrier of T2, the carrier of [:(T1 | S2),T2:]:] is non empty set

bool [: the carrier of T2, the carrier of [:(T1 | S2),T2:]:] is non empty set

S1 is Relation-like the carrier of T2 -defined the carrier of (T1 | S2) -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of (T1 | S2):]

<:S1,(id T2):> is Relation-like the carrier of T2 -defined [: the carrier of (T1 | S2), the carrier of T2:] -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2,[: the carrier of (T1 | S2), the carrier of T2:]:]

[: the carrier of (T1 | S2), the carrier of T2:] is non empty set

[: the carrier of T2,[: the carrier of (T1 | S2), the carrier of T2:]:] is non empty set

bool [: the carrier of T2,[: the carrier of (T1 | S2), the carrier of T2:]:] is non empty set

X is Relation-like the carrier of T2 -defined the carrier of [:(T1 | S2),T2:] -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of [:(T1 | S2),T2:]:]

rng X is Element of bool the carrier of [:(T1 | S2),T2:]

bool the carrier of [:(T1 | S2),T2:] is non empty set

Q9 is set

A is set

A is set

[A,A] is non empty set

{A,A} is non empty set

{A} is non empty trivial set

{{A,A},{A}} is non empty set

[S1,A] is non empty set

{S1,A} is non empty set

{S1} is non empty trivial set

{{S1,A},{S1}} is non empty set

S1 . A is set

( the carrier of T2 --> S1) . A is set

dom X is Element of bool the carrier of T2

X . A is set

(id T2) . A is set

[(S1 . A),((id T2) . A)] is non empty set

{(S1 . A),((id T2) . A)} is non empty set

{(S1 . A)} is non empty trivial set

{{(S1 . A),((id T2) . A)},{(S1 . A)}} is non empty set

rng S1 is Element of bool the carrier of (T1 | S2)

bool the carrier of (T1 | S2) is non empty set

[:(rng S1),(rng (id T2)):] is Element of bool the carrier of [:(T1 | S2),T2:]

[:S2, the carrier of T2:] is non empty set

dom S2 is Element of bool the carrier of [:(T1 | {S1}),T2:]

bool the carrier of [:(T1 | {S1}),T2:] is non empty set

dom S1 is Element of bool the carrier of T2

dom (id T2) is Element of bool the carrier of T2

S2 * X is Relation-like the carrier of T2 -defined the carrier of T2 -valued Function-like Element of bool [: the carrier of T2, the carrier of T2:]

id (rng S2) is Relation-like rng S2 -defined rng S2 -valued total quasi_total Element of bool [:(rng S2),(rng S2):]

[:(rng S2),(rng S2):] is set

bool [:(rng S2),(rng S2):] is non empty set

S2 " is Relation-like Function-like set

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

T2 is non empty TopSpace-like TopStruct

the carrier of T2 is non empty set

S1 is Element of the carrier of T1

{S1} is non empty trivial compact Element of bool the carrier of T1

bool the carrier of T1 is non empty set

T1 | {S1} is non empty strict TopSpace-like SubSpace of T1

[:T2,(T1 | {S1}):] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,(T1 | {S1}):] is non empty set

[: the carrier of [:T2,(T1 | {S1}):], the carrier of T2:] is non empty set

bool [: the carrier of [:T2,(T1 | {S1}):], the carrier of T2:] is non empty set

[: the carrier of T2,{S1}:] is non empty set

pr1 ( the carrier of T2,{S1}) is Relation-like [: the carrier of T2,{S1}:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T2,{S1}:], the carrier of T2:]

[:[: the carrier of T2,{S1}:], the carrier of T2:] is non empty set

bool [:[: the carrier of T2,{S1}:], the carrier of T2:] is non empty set

S2 is Relation-like the carrier of [:T2,(T1 | {S1}):] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:T2,(T1 | {S1}):], the carrier of T2:]

dom S2 is Element of bool the carrier of [:T2,(T1 | {S1}):]

bool the carrier of [:T2,(T1 | {S1}):] is non empty set

[#] [:T2,(T1 | {S1}):] is non empty non proper open closed dense non boundary Element of bool the carrier of [:T2,(T1 | {S1}):]

rng S2 is Element of bool the carrier of T2

bool the carrier of T2 is non empty set

[#] T2 is non empty non proper open closed dense non boundary Element of bool the carrier of T2

S2 " is Relation-like the carrier of T2 -defined the carrier of [:T2,(T1 | {S1}):] -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of [:T2,(T1 | {S1}):]:]

[: the carrier of T2, the carrier of [:T2,(T1 | {S1}):]:] is non empty set

bool [: the carrier of T2, the carrier of [:T2,(T1 | {S1}):]:] is non empty set

the carrier of (T1 | {S1}) is non empty set

T2 is non empty Element of bool the carrier of T1

T1 | T2 is non empty strict TopSpace-like SubSpace of T1

the carrier of (T1 | T2) is non empty set

[: the carrier of T2, the carrier of (T1 | T2):] is non empty set

bool [: the carrier of T2, the carrier of (T1 | T2):] is non empty set

T2 --> S1 is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of T1:]

[: the carrier of T2, the carrier of T1:] is non empty set

bool [: the carrier of T2, the carrier of T1:] is non empty set

the carrier of T2 --> S1 is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of T1:]

[:T2,(T1 | T2):] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,(T1 | T2):] is non empty set

[: the carrier of T2, the carrier of [:T2,(T1 | T2):]:] is non empty set

bool [: the carrier of T2, the carrier of [:T2,(T1 | T2):]:] is non empty set

id T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued Function-like non empty total quasi_total continuous being_homeomorphism open Element of bool [: the carrier of T2, the carrier of T2:]

[: the carrier of T2, the carrier of T2:] is non empty set

bool [: the carrier of T2, the carrier of T2:] is non empty set

id the carrier of T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued non empty total quasi_total Element of bool [: the carrier of T2, the carrier of T2:]

S2 is Relation-like the carrier of T2 -defined the carrier of (T1 | T2) -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of (T1 | T2):]

<:(id T2),S2:> is Relation-like the carrier of T2 -defined [: the carrier of T2, the carrier of (T1 | T2):] -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2,[: the carrier of T2, the carrier of (T1 | T2):]:]

[: the carrier of T2,[: the carrier of T2, the carrier of (T1 | T2):]:] is non empty set

bool [: the carrier of T2,[: the carrier of T2, the carrier of (T1 | T2):]:] is non empty set

S1 is Relation-like the carrier of T2 -defined the carrier of [:T2,(T1 | T2):] -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of [:T2,(T1 | T2):]:]

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

T2 is non empty TopSpace-like TopStruct

the carrier of T2 is non empty set

S1 is Element of the carrier of T1

{S1} is non empty trivial compact Element of bool the carrier of T1

bool the carrier of T1 is non empty set

T1 | {S1} is non empty strict TopSpace-like SubSpace of T1

[:(T1 | {S1}),T2:] is non empty strict TopSpace-like TopStruct

the carrier of [:(T1 | {S1}),T2:] is non empty set

[: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:] is non empty set

bool [: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:] is non empty set

[:{S1}, the carrier of T2:] is non empty set

pr2 ({S1}, the carrier of T2) is Relation-like [:{S1}, the carrier of T2:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [:[:{S1}, the carrier of T2:], the carrier of T2:]

[:[:{S1}, the carrier of T2:], the carrier of T2:] is non empty set

bool [:[:{S1}, the carrier of T2:], the carrier of T2:] is non empty set

S2 is Relation-like the carrier of [:(T1 | {S1}),T2:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:]

dom S2 is Element of bool the carrier of [:(T1 | {S1}),T2:]

bool the carrier of [:(T1 | {S1}),T2:] is non empty set

[#] [:(T1 | {S1}),T2:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:(T1 | {S1}),T2:]

rng S2 is Element of bool the carrier of T2

bool the carrier of T2 is non empty set

[#] T2 is non empty non proper open closed dense non boundary Element of bool the carrier of T2

S2 " is Relation-like the carrier of T2 -defined the carrier of [:(T1 | {S1}),T2:] -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of [:(T1 | {S1}),T2:]:]

[: the carrier of T2, the carrier of [:(T1 | {S1}),T2:]:] is non empty set

bool [: the carrier of T2, the carrier of [:(T1 | {S1}),T2:]:] is non empty set

the carrier of (T1 | {S1}) is non empty set

T2 is non empty Element of bool the carrier of T1

T1 | T2 is non empty strict TopSpace-like SubSpace of T1

the carrier of (T1 | T2) is non empty set

[: the carrier of T2, the carrier of (T1 | T2):] is non empty set

bool [: the carrier of T2, the carrier of (T1 | T2):] is non empty set

T2 --> S1 is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of T1:]

[: the carrier of T2, the carrier of T1:] is non empty set

bool [: the carrier of T2, the carrier of T1:] is non empty set

the carrier of T2 --> S1 is Relation-like the carrier of T2 -defined the carrier of T1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2, the carrier of T1:]

[:(T1 | T2),T2:] is non empty strict TopSpace-like TopStruct

the carrier of [:(T1 | T2),T2:] is non empty set

[: the carrier of T2, the carrier of [:(T1 | T2),T2:]:] is non empty set

bool [: the carrier of T2, the carrier of [:(T1 | T2),T2:]:] is non empty set

S2 is Relation-like the carrier of T2 -defined the carrier of (T1 | T2) -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of (T1 | T2):]

id T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued Function-like non empty total quasi_total continuous being_homeomorphism open Element of bool [: the carrier of T2, the carrier of T2:]

[: the carrier of T2, the carrier of T2:] is non empty set

bool [: the carrier of T2, the carrier of T2:] is non empty set

id the carrier of T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued non empty total quasi_total Element of bool [: the carrier of T2, the carrier of T2:]

<:S2,(id T2):> is Relation-like the carrier of T2 -defined [: the carrier of (T1 | T2), the carrier of T2:] -valued Function-like non empty total quasi_total Element of bool [: the carrier of T2,[: the carrier of (T1 | T2), the carrier of T2:]:]

[: the carrier of (T1 | T2), the carrier of T2:] is non empty set

[: the carrier of T2,[: the carrier of (T1 | T2), the carrier of T2:]:] is non empty set

bool [: the carrier of T2,[: the carrier of (T1 | T2), the carrier of T2:]:] is non empty set

S1 is Relation-like the carrier of T2 -defined the carrier of [:(T1 | T2),T2:] -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of T2, the carrier of [:(T1 | T2),T2:]:]

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

bool the carrier of T1 is non empty set

T2 is non empty TopSpace-like compact TopStruct

[:T1,T2:] is non empty strict TopSpace-like TopStruct

the carrier of [:T1,T2:] is non empty set

bool the carrier of [:T1,T2:] is non empty set

the carrier of T2 is non empty set

bool the carrier of T2 is non empty set

S1 is open Element of bool the carrier of [:T1,T2:]

S2 is set

{S2} is non empty trivial set

[:{S2}, the carrier of T2:] is non empty set

the Element of the carrier of T2 is Element of the carrier of T2

[: the carrier of T1, the carrier of T2:] is non empty set

[S2, the Element of the carrier of T2] is non empty set

{S2, the Element of the carrier of T2} is non empty set

{{S2, the Element of the carrier of T2},{S2}} is non empty set

T2 is Element of the carrier of T1

{T2} is non empty trivial compact Element of bool the carrier of T1

[:{T2}, the carrier of T2:] is non empty set

Base-Appr S1 is open Element of bool (bool the carrier of [:T1,T2:])

bool (bool the carrier of [:T1,T2:]) is non empty set

union (Base-Appr S1) is Element of bool the carrier of [:T1,T2:]

S2 is set

[S2,S2] is non empty set

{S2,S2} is non empty set

{{S2,S2},{S2}} is non empty set

S1 is set

{ [:b

X is Element of bool the carrier of T1

Q9 is Element of bool the carrier of T2

[:X,Q9:] is Element of bool the carrier of [:T1,T2:]

S2 is set

[S2,S2] is non empty set

{S2,S2} is non empty set

{{S2,S2},{S2}} is non empty set

S1 is Element of bool the carrier of T1

X is Element of bool the carrier of T2

[:S1,X:] is Element of bool the carrier of [:T1,T2:]

[S1,X] is non empty Element of [:(bool the carrier of T1),(bool the carrier of T2):]

[:(bool the carrier of T1),(bool the carrier of T2):] is non empty set

{S1,X} is non empty set

{S1} is non empty trivial set

{{S1,X},{S1}} is non empty set

Q9 is Element of bool the carrier of T1

A is Element of bool the carrier of T2

[Q9,A] is non empty Element of [:(bool the carrier of T1),(bool the carrier of T2):]

{Q9,A} is non empty set

{Q9} is non empty trivial set

{{Q9,A},{Q9}} is non empty set

[:Q9,A:] is Element of bool the carrier of [:T1,T2:]

S2 is Relation-like the carrier of T2 -defined Function-like total set

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

bool the carrier of T1 is non empty set

T2 is non empty TopSpace-like compact TopStruct

[:T2,T1:] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,T1:] is non empty set

bool the carrier of [:T2,T1:] is non empty set

[#] T2 is non empty non proper open closed dense non boundary Element of bool the carrier of T2

the carrier of T2 is non empty set

bool the carrier of T2 is non empty set

S1 is open Element of bool the carrier of [:T2,T1:]

{ b

S2 is set

{S2} is non empty trivial set

[:([#] T2),{S2}:] is non empty set

the Element of the carrier of T2 is Element of the carrier of T2

[: the carrier of T2, the carrier of T1:] is non empty set

[ the Element of the carrier of T2,S2] is non empty set

{ the Element of the carrier of T2,S2} is non empty set

{ the Element of the carrier of T2} is non empty trivial set

{{ the Element of the carrier of T2,S2},{ the Element of the carrier of T2}} is non empty set

[: the carrier of T2,{S2}:] is non empty set

Int S1 is open Element of bool the carrier of [:T2,T1:]

T2 is Element of the carrier of T1

{T2} is non empty trivial compact Element of bool the carrier of T1

[:([#] T2),{T2}:] is non empty Element of bool the carrier of [:T2,T1:]

S2 is a_neighborhood of [#] T2

S1 is a_neighborhood of T2

[:S2,S1:] is a_neighborhood of [:([#] T2),{T2}:]

Int S1 is open Element of bool the carrier of T1

X is open Element of bool the carrier of T1

Int S2 is open Element of bool the carrier of T2

Q9 is set

{Q9} is non empty trivial set

A is Element of the carrier of T1

{A} is non empty trivial compact Element of bool the carrier of T1

[:([#] T2),{A}:] is non empty Element of bool the carrier of [:T2,T1:]

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

the topology of T1 is non empty open Element of bool (bool the carrier of T1)

bool the carrier of T1 is non empty set

bool (bool the carrier of T1) is non empty set

T2 is non empty TopSpace-like compact TopStruct

[:T2,T1:] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,T1:] is non empty set

bool the carrier of [:T2,T1:] is non empty set

[#] T2 is non empty non proper open closed dense non boundary Element of bool the carrier of T2

the carrier of T2 is non empty set

bool the carrier of T2 is non empty set

S1 is open Element of bool the carrier of [:T2,T1:]

{ b

S2 is set

T2 is Element of the carrier of T1

{T2} is non empty trivial compact Element of bool the carrier of T1

[:([#] T2),{T2}:] is non empty Element of bool the carrier of [:T2,T1:]

S2 is Element of bool the carrier of T1

bool S2 is non empty Element of bool (bool S2)

bool S2 is non empty set

bool (bool S2) is non empty set

T2 is set

S2 is set

S2 is Element of bool (bool S2)

union S2 is Element of bool S2

S1 is set

X is Element of the carrier of T1

{X} is non empty trivial compact Element of bool the carrier of T1

[:([#] T2),{X}:] is non empty Element of bool the carrier of [:T2,T1:]

X is open Element of bool the carrier of T1

bool the carrier of T1 is non empty Element of bool (bool the carrier of T1)

S1 is Element of bool (bool the carrier of T1)

X is set

Q9 is set

A is Element of bool the carrier of T1

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

T2 is non empty TopSpace-like TopStruct

S1 is Element of the carrier of T1

{S1} is non empty trivial compact Element of bool the carrier of T1

bool the carrier of T1 is non empty set

T1 | {S1} is non empty strict TopSpace-like SubSpace of T1

[:(T1 | {S1}),T2:] is non empty strict TopSpace-like TopStruct

the carrier of [:(T1 | {S1}),T2:] is non empty set

the carrier of (T1 | {S1}) is non empty set

the carrier of T2 is non empty set

[: the carrier of (T1 | {S1}), the carrier of T2:] is non empty set

[:{S1}, the carrier of T2:] is non empty set

[: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:] is non empty set

bool [: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:] is non empty set

pr2 ({S1}, the carrier of T2) is Relation-like [:{S1}, the carrier of T2:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [:[:{S1}, the carrier of T2:], the carrier of T2:]

[:[:{S1}, the carrier of T2:], the carrier of T2:] is non empty set

bool [:[:{S1}, the carrier of T2:], the carrier of T2:] is non empty set

S2 is Relation-like the carrier of [:(T1 | {S1}),T2:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:(T1 | {S1}),T2:], the carrier of T2:]

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

bool the carrier of T1 is non empty set

T2 is non empty TopSpace-like TopStruct

S1 is Element of the carrier of T1

{S1} is non empty trivial compact Element of bool the carrier of T1

S2 is non empty Element of bool the carrier of T1

T1 | S2 is non empty strict TopSpace-like SubSpace of T1

[:T2,(T1 | S2):] is non empty strict TopSpace-like TopStruct

[:(T1 | S2),T2:] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,(T1 | S2):] is non empty set

the carrier of [:(T1 | S2),T2:] is non empty set

[: the carrier of [:T2,(T1 | S2):], the carrier of [:(T1 | S2),T2:]:] is non empty set

bool [: the carrier of [:T2,(T1 | S2):], the carrier of [:(T1 | S2),T2:]:] is non empty set

S2 is Relation-like the carrier of [:T2,(T1 | S2):] -defined the carrier of [:(T1 | S2),T2:] -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:T2,(T1 | S2):], the carrier of [:(T1 | S2),T2:]:]

the carrier of T2 is non empty set

[: the carrier of [:(T1 | S2),T2:], the carrier of T2:] is non empty set

bool [: the carrier of [:(T1 | S2),T2:], the carrier of T2:] is non empty set

T2 is Relation-like the carrier of [:(T1 | S2),T2:] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:(T1 | S2),T2:], the carrier of T2:]

[: the carrier of [:T2,(T1 | S2):], the carrier of T2:] is non empty set

bool [: the carrier of [:T2,(T1 | S2):], the carrier of T2:] is non empty set

T2 * S2 is Relation-like the carrier of [:T2,(T1 | S2):] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:T2,(T1 | S2):], the carrier of T2:]

S2 is Relation-like the carrier of [:T2,(T1 | S2):] -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:T2,(T1 | S2):], the carrier of T2:]

T1 is non empty TopSpace-like TopStruct

T2 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

the carrier of T2 is non empty set

[: the carrier of T1, the carrier of T2:] is non empty set

bool [: the carrier of T1, the carrier of T2:] is non empty set

S1 is Relation-like the carrier of T1 -defined the carrier of T2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of T1, the carrier of T2:]

rng S1 is Element of bool the carrier of T2

bool the carrier of T2 is non empty set

[#] T2 is non empty non proper open closed dense non boundary Element of bool the carrier of T2

T1 is TopSpace-like TopStruct

T2 is TopSpace-like TopStruct

[:T2,T1:] is strict TopSpace-like TopStruct

S1 is TopSpace-like SubSpace of T1

[:T2,S1:] is strict TopSpace-like TopStruct

the carrier of [:T2,S1:] is set

the carrier of T2 is set

the carrier of S1 is set

[: the carrier of T2, the carrier of S1:] is set

the carrier of [:T2,T1:] is set

the carrier of T1 is set

[: the carrier of T2, the carrier of T1:] is set

bool the carrier of [:T2,S1:] is non empty set

the topology of [:T2,S1:] is non empty open Element of bool (bool the carrier of [:T2,S1:])

bool (bool the carrier of [:T2,S1:]) is non empty set

bool the carrier of [:T2,T1:] is non empty set

the topology of [:T2,T1:] is non empty open Element of bool (bool the carrier of [:T2,T1:])

bool (bool the carrier of [:T2,T1:]) is non empty set

[#] [:T2,S1:] is non proper open closed dense Element of bool the carrier of [:T2,S1:]

S2 is Element of bool the carrier of [:T2,S1:]

S1 is Element of bool the carrier of [:T2,S1:]

bool the carrier of T2 is non empty set

bool the carrier of S1 is non empty set

X is Element of bool (bool the carrier of [:T2,S1:])

union X is Element of bool the carrier of [:T2,S1:]

bool the carrier of T1 is non empty set

[#] S1 is non proper open closed dense Element of bool the carrier of S1

{ [:b

( b

bool the carrier of [:T2,T1:] is non empty Element of bool (bool the carrier of [:T2,T1:])

A is set

A is Element of bool the carrier of T2

AA is Element of bool the carrier of T1

[:A,AA:] is Element of bool the carrier of [:T2,T1:]

AA is Element of bool the carrier of S1

AA /\ ([#] S1) is Element of bool the carrier of S1

[:A,AA:] is Element of bool the carrier of [:T2,S1:]

A is Element of bool (bool the carrier of [:T2,T1:])

A is Element of bool (bool the carrier of [:T2,T1:])

union A is Element of bool the carrier of [:T2,T1:]

(union A) /\ ([#] [:T2,S1:]) is Element of bool the carrier of [:T2,S1:]

AA is set

AA is set

AA is Element of bool the carrier of [:T2,S1:]

s is Element of bool the carrier of T2

A1 is Element of bool the carrier of S1

[:s,A1:] is Element of bool the carrier of [:T2,S1:]

the topology of S1 is non empty open Element of bool (bool the carrier of S1)

bool (bool the carrier of S1) is non empty set

the topology of T1 is non empty open Element of bool (bool the carrier of T1)

bool (bool the carrier of T1) is non empty set

A1 is Element of bool the carrier of T1

A1 /\ ([#] S1) is Element of bool the carrier of S1

X1 is set

Y1 is set

[X1,Y1] is non empty set

{X1,Y1} is non empty set

{X1} is non empty trivial set

{{X1,Y1},{X1}} is non empty set

D2 is Element of bool the carrier of T1

[:s,D2:] is Element of bool the carrier of [:T2,T1:]

AA is set

{AA} is non empty trivial set

AA is Element of bool the carrier of T2

s is Element of bool the carrier of T1

[:AA,s:] is Element of bool the carrier of [:T2,T1:]

s /\ ([#] S1) is Element of bool the carrier of S1

A1 is set

A1 is Element of bool (bool the carrier of [:T2,T1:])

the topology of T2 is non empty open Element of bool (bool the carrier of T2)

bool (bool the carrier of T2) is non empty set

the topology of T1 is non empty open Element of bool (bool the carrier of T1)

bool (bool the carrier of T1) is non empty set

{ [:b

A1 is set

X1 is Element of bool the carrier of S1

[:AA,X1:] is Element of bool the carrier of [:T2,S1:]

union A1 is Element of bool the carrier of [:T2,T1:]

{ (union b

AA is set

AA is set

AA is Element of bool the carrier of T2

s is Element of bool the carrier of T1

[:AA,s:] is Element of bool the carrier of [:T2,T1:]

s /\ ([#] S1) is Element of bool the carrier of S1

A1 is Element of bool the carrier of S1

[:AA,A1:] is Element of bool the carrier of [:T2,S1:]

A1 is Element of bool the carrier of S1

[:AA,A1:] is Element of bool the carrier of [:T2,S1:]

A1 is set

X1 is set

[A1,X1] is non empty set

{A1,X1} is non empty set

{A1} is non empty trivial set

{{A1,X1},{A1}} is non empty set

X is Element of bool the carrier of [:T2,T1:]

X /\ ([#] [:T2,S1:]) is Element of bool the carrier of [:T2,S1:]

Q9 is Element of bool the carrier of [:T2,T1:]

A is Element of bool (bool the carrier of [:T2,T1:])

union A is Element of bool the carrier of [:T2,T1:]

T2 is Element of bool the carrier of [:T2,T1:]

[:T2,T1:] | T2 is strict TopSpace-like SubSpace of [:T2,T1:]

the carrier of ([:T2,T1:] | T2) is set

bool the carrier of ([:T2,T1:] | T2) is non empty set

bool (bool the carrier of ([:T2,T1:] | T2)) is non empty set

A is Element of bool (bool the carrier of [:T2,T1:])

A | T2 is Element of bool (bool the carrier of ([:T2,T1:] | T2))

AA is Element of bool (bool the carrier of ([:T2,T1:] | T2))

AA is Element of bool (bool the carrier of [:T2,S1:])

AA is Element of bool (bool the carrier of [:T2,S1:])

s is set

A1 is Element of bool the carrier of ([:T2,T1:] | T2)

A1 is Element of bool the carrier of [:T2,T1:]

A1 /\ T2 is Element of bool the carrier of [:T2,T1:]

X1 is Element of bool the carrier of T2

Y1 is Element of bool the carrier of T1

[:X1,Y1:] is Element of bool the carrier of [:T2,T1:]

Y1 /\ ([#] S1) is Element of bool the carrier of S1

the topology of T1 is non empty open Element of bool (bool the carrier of T1)

bool (bool the carrier of T1) is non empty set

D2 is Element of bool the carrier of S1

the topology of S1 is non empty open Element of bool (bool the carrier of S1)

bool (bool the carrier of S1) is non empty set

[#] T2 is non proper open closed dense Element of bool the carrier of T2

[:([#] T2),([#] S1):] is Element of bool the carrier of [:T2,S1:]

X1 /\ ([#] T2) is Element of bool the carrier of T2

[:(X1 /\ ([#] T2)),(Y1 /\ ([#] S1)):] is Element of bool the carrier of [:T2,S1:]

union A is Element of bool the carrier of [:T2,T1:]

(union A) /\ T2 is Element of bool the carrier of [:T2,T1:]

union AA is Element of bool the carrier of [:T2,S1:]

s is set

A1 is set

A1 /\ T2 is Element of bool the carrier of [:T2,T1:]

A1 is Element of bool the carrier of [:T2,T1:]

A1 /\ T2 is Element of bool the carrier of [:T2,T1:]

[#] [:T2,T1:] is non proper open closed dense Element of bool the carrier of [:T2,T1:]

T2 is TopSpace-like TopStruct

T1 is TopSpace-like TopStruct

[:T2,T1:] is strict TopSpace-like TopStruct

the carrier of [:T2,T1:] is set

bool the carrier of [:T2,T1:] is non empty set

the carrier of T1 is set

bool the carrier of T1 is non empty set

[#] T2 is non proper open closed dense Element of bool the carrier of T2

the carrier of T2 is set

bool the carrier of T2 is non empty set

S1 is Element of bool the carrier of [:T2,T1:]

[:T2,T1:] | S1 is strict TopSpace-like SubSpace of [:T2,T1:]

the carrier of ([:T2,T1:] | S1) is set

the topology of ([:T2,T1:] | S1) is non empty open Element of bool (bool the carrier of ([:T2,T1:] | S1))

bool the carrier of ([:T2,T1:] | S1) is non empty set

bool (bool the carrier of ([:T2,T1:] | S1)) is non empty set

TopStruct(# the carrier of ([:T2,T1:] | S1), the topology of ([:T2,T1:] | S1) #) is strict TopSpace-like TopStruct

S2 is Element of bool the carrier of T1

[:([#] T2),S2:] is Element of bool the carrier of [:T2,T1:]

T1 | S2 is strict TopSpace-like SubSpace of T1

[:T2,(T1 | S2):] is strict TopSpace-like TopStruct

the carrier of [:T2,(T1 | S2):] is set

the topology of [:T2,(T1 | S2):] is non empty open Element of bool (bool the carrier of [:T2,(T1 | S2):])

bool the carrier of [:T2,(T1 | S2):] is non empty set

bool (bool the carrier of [:T2,(T1 | S2):]) is non empty set

TopStruct(# the carrier of [:T2,(T1 | S2):], the topology of [:T2,(T1 | S2):] #) is strict TopSpace-like TopStruct

S2 is TopSpace-like SubSpace of [:T2,T1:]

the carrier of S2 is set

the carrier of (T1 | S2) is set

[: the carrier of T2, the carrier of (T1 | S2):] is set

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

T2 is non empty TopSpace-like compact TopStruct

[:T2,T1:] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,T1:] is non empty set

bool the carrier of [:T2,T1:] is non empty set

[#] T2 is non empty non proper open closed dense non boundary Element of bool the carrier of T2

the carrier of T2 is non empty set

bool the carrier of T2 is non empty set

S1 is Element of the carrier of T1

{S1} is non empty trivial compact Element of bool the carrier of T1

bool the carrier of T1 is non empty set

[:([#] T2),{S1}:] is non empty Element of bool the carrier of [:T2,T1:]

S2 is Element of bool the carrier of [:T2,T1:]

S2 is non empty Element of bool the carrier of T1

T1 | S2 is non empty strict TopSpace-like SubSpace of T1

[:T2,(T1 | S2):] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,(T1 | S2):] is non empty set

the topology of [:T2,(T1 | S2):] is non empty open Element of bool (bool the carrier of [:T2,(T1 | S2):])

bool the carrier of [:T2,(T1 | S2):] is non empty set

bool (bool the carrier of [:T2,(T1 | S2):]) is non empty set

TopStruct(# the carrier of [:T2,(T1 | S2):], the topology of [:T2,(T1 | S2):] #) is non empty strict TopSpace-like TopStruct

[:T2,T1:] | S2 is strict TopSpace-like SubSpace of [:T2,T1:]

the carrier of ([:T2,T1:] | S2) is set

the topology of ([:T2,T1:] | S2) is non empty open Element of bool (bool the carrier of ([:T2,T1:] | S2))

bool the carrier of ([:T2,T1:] | S2) is non empty set

bool (bool the carrier of ([:T2,T1:] | S2)) is non empty set

TopStruct(# the carrier of ([:T2,T1:] | S2), the topology of ([:T2,T1:] | S2) #) is strict TopSpace-like TopStruct

T1 is non empty TopSpace-like TopStruct

the carrier of T1 is non empty set

T2 is non empty TopSpace-like compact TopStruct

S1 is Element of the carrier of T1

{S1} is non empty trivial compact Element of bool the carrier of T1

bool the carrier of T1 is non empty set

T1 | {S1} is non empty strict TopSpace-like SubSpace of T1

[:T2,(T1 | {S1}):] is non empty strict TopSpace-like TopStruct

T1 is non empty TopSpace-like compact TopStruct

the carrier of T1 is non empty set

bool the carrier of T1 is non empty set

bool (bool the carrier of T1) is non empty set

T2 is non empty TopSpace-like compact TopStruct

[#] T2 is non empty non proper open closed dense non boundary Element of bool the carrier of T2

the carrier of T2 is non empty set

bool the carrier of T2 is non empty set

[:T2,T1:] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,T1:] is non empty set

[#] [:T2,T1:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:T2,T1:]

bool the carrier of [:T2,T1:] is non empty set

Base-Appr ([#] [:T2,T1:]) is open Element of bool (bool the carrier of [:T2,T1:])

bool (bool the carrier of [:T2,T1:]) is non empty set

union (Base-Appr ([#] [:T2,T1:])) is Element of bool the carrier of [:T2,T1:]

{ b

[#] T1 is non empty non proper open closed dense non boundary Element of bool the carrier of T1

S1 is Element of bool (bool the carrier of T1)

S2 is Element of bool the carrier of T1

S2 is open Element of bool the carrier of T1

[:([#] T2),S2:] is Element of bool the carrier of [:T2,T1:]

union S1 is Element of bool the carrier of T1

S2 is set

S2 is Element of the carrier of T1

{S2} is non empty trivial compact Element of bool the carrier of T1

[:([#] T2),{S2}:] is non empty Element of bool the carrier of [:T2,T1:]

T2 is Element of bool the carrier of [:T2,T1:]

S2 is Element of bool (bool the carrier of [:T2,T1:])

union S2 is Element of bool the carrier of [:T2,T1:]

{ b

Q9 is set

A is Element of the carrier of T1

{A} is non empty trivial compact Element of bool the carrier of T1

[:([#] T2),{A}:] is non empty Element of bool the carrier of [:T2,T1:]

Q9 is Element of bool the carrier of T1

[:([#] T2),Q9:] is Element of bool the carrier of [:T2,T1:]

A is set

A is set

AA is set

[A,AA] is non empty set

{A,AA} is non empty set

{A} is non empty trivial set

{{A,AA},{A}} is non empty set

AA is Element of the carrier of T1

{AA} is non empty trivial compact Element of bool the carrier of T1

[:([#] T2),{AA}:] is non empty Element of bool the carrier of [:T2,T1:]

the topology of T1 is non empty open Element of bool (bool the carrier of T1)

T1 is non empty TopSpace-like compact TopStruct

the carrier of T1 is non empty set

bool the carrier of T1 is non empty set

bool (bool the carrier of T1) is non empty set

T2 is non empty TopSpace-like compact TopStruct

[:T2,T1:] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,T1:] is non empty set

bool the carrier of [:T2,T1:] is non empty set

bool (bool the carrier of [:T2,T1:]) is non empty set

[#] T2 is non empty non proper open closed dense non boundary Element of bool the carrier of T2

the carrier of T2 is non empty set

bool the carrier of T2 is non empty set

S1 is Element of bool (bool the carrier of T1)

S2 is Element of bool (bool the carrier of [:T2,T1:])

{ b

( b

S2 is Element of bool the carrier of T1

T2 is open Element of bool the carrier of T1

S2 is Element of bool (bool the carrier of [:T2,T1:])

[:([#] T2),T2:] is Element of bool the carrier of [:T2,T1:]

union S2 is Element of bool the carrier of [:T2,T1:]

union S2 is Element of bool the carrier of [:T2,T1:]

[#] [:T2,T1:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:T2,T1:]

[#] T1 is non empty non proper open closed dense non boundary Element of bool the carrier of T1

union S1 is Element of bool the carrier of T1

S2 is set

T2 is Element of the carrier of T1

{T2} is non empty trivial compact Element of bool the carrier of T1

[:([#] T2),{T2}:] is non empty Element of bool the carrier of [:T2,T1:]

S2 is Element of bool the carrier of [:T2,T1:]

S1 is Element of bool (bool the carrier of [:T2,T1:])

union S1 is Element of bool the carrier of [:T2,T1:]

{ b

A is set

A is Element of the carrier of T1

{A} is non empty trivial compact Element of bool the carrier of T1

[:([#] T2),{A}:] is non empty Element of bool the carrier of [:T2,T1:]

A is Element of bool the carrier of T1

[:([#] T2),A:] is Element of bool the carrier of [:T2,T1:]

A is set

AA is set

AA is set

[AA,AA] is non empty set

{AA,AA} is non empty set

{AA} is non empty trivial set

{{AA,AA},{AA}} is non empty set

AA is Element of the carrier of T1

{AA} is non empty trivial compact Element of bool the carrier of T1

[:([#] T2),{AA}:] is non empty Element of bool the carrier of [:T2,T1:]

the topology of T1 is non empty open Element of bool (bool the carrier of T1)

A is Element of bool (bool the carrier of [:T2,T1:])

union A is Element of bool the carrier of [:T2,T1:]

T1 is non empty TopSpace-like compact TopStruct

the carrier of T1 is non empty set

bool the carrier of T1 is non empty set

bool (bool the carrier of T1) is non empty set

T2 is non empty TopSpace-like compact TopStruct

[:T2,T1:] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,T1:] is non empty set

bool the carrier of [:T2,T1:] is non empty set

bool (bool the carrier of [:T2,T1:]) is non empty set

[#] T2 is non empty non proper open closed dense non boundary Element of bool the carrier of T2

the carrier of T2 is non empty set

bool the carrier of T2 is non empty set

S1 is Element of bool (bool the carrier of T1)

S2 is Element of bool (bool the carrier of [:T2,T1:])

{ b

( b

S2 is Element of bool (bool the carrier of T1)

T2 is non empty TopSpace-like compact TopStruct

T1 is non empty TopSpace-like compact TopStruct

[:T2,T1:] is non empty strict TopSpace-like TopStruct

the carrier of [:T2,T1:] is non empty set

bool the carrier of [:T2,T1:] is non empty set

bool (bool the carrier of [:T2,T1:]) is non empty set

S1 is Element of bool (bool the carrier of [:T2,T1:])

the carrier of T1 is non empty set

bool the carrier of T1 is non empty set

[#] T2 is non empty non proper open closed dense non boundary Element of bool the carrier of T2

the carrier of T2 is non empty set

bool the carrier of T2 is non empty set

{ b

( b

bool the carrier of T1 is non empty Element of bool (bool the carrier of T1)

bool (bool the carrier of T1) is non empty set

S2 is set

T2 is open Element of bool the carrier of T1

S2 is Element of bool (bool the carrier of [:T2,T1:])

[:([#] T2),T2:] is Element of bool the carrier of [:T2,T1:]

union S2 is Element of bool the carrier of [:T2,T1:]

S2 is Element of bool (bool the carrier of T1)

T2 is Element of bool (bool the carrier of T1)

S2 is Element of bool (bool the carrier of T1)

{ H

bool the carrier of [:T2,T1:] is non empty Element of bool (bool the carrier of [:T2,T1:])

X is set

Q9 is Element of bool the carrier of T1

[:([#] T2),Q9:] is set

[:([#] T2),Q9:] is Element of bool the carrier of [:T2,T1:]

X is Element of bool (bool the carrier of [:T2,T1:])

A is set

[:([#] T2),A:] is set

A is open Element of bool the carrier of T1

AA is Element of bool (bool the carrier of [:T2,T1:])

[:([#] T2),A:] is Element of bool the carrier of [:T2,T1:]

union AA is Element of bool the carrier of [:T2,T1:]

A is Relation-like Function-like set

dom A is set

rng A is set

union (rng A) is set

AA is set

AA is set

AA is set

A . AA is set

[:([#] T2),AA:] is set

s is Element of bool (bool the carrier of [:T2,T1:])

union s is Element of bool the carrier of [:T2,T1:]

AA is set

AA is Element of bool (bool the carrier of [:T2,T1:])

AA is Element of bool (bool the carrier of [:T2,T1:])

Q9 is Element of bool (bool the carrier of [:T2,T1:])

union Q9 is Element of bool the carrier of [:T2,T1:]

union S2 is Element of bool the carrier of T1

[:([#] T2),(union S2):] is Element of bool the carrier of [:T2,T1:]

AA is set

s is set

A1 is Element of bool the carrier of T1

[:([#] T2),A1:] is Element of bool the carrier of [:T2,T1:]

A1 is set

X1 is set

[A1,X1] is non empty set

{A1,X1} is non empty set

{A1} is non empty trivial set

{{A1,X1},{A1}} is non empty set

AA is set

s is set

A1 is set

[s,A1] is non empty set

{s,A1} is non empty