:: 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₁,b₂:] where b₁ is Element of bool the carrier of T1, b₂ is Element of bool the carrier of T2 : ( [:b₁,b₂:] c= S1 & b₁ is open & b₂ is open ) } is set
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₁ where b₁ is Element of the carrier of T1 : [:([#] T2),{b₁}:] c= S1 } is set
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₁ where b₁ is Element of the carrier of T1 : [:([#] T2),{b₁}:] c= S1 } is set
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₂:] where b₁ is Element of bool the carrier of T2, b₂ is Element of bool the carrier of T1 : ex b₃ being Element of bool the carrier of S1 st
( b₃ = b₂ /\ ([#] S1) & b₁ is open & b₂ is open & [:b₁,b₃:] in X ) } is set
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₁,b₂:] where b₁ is Element of bool the carrier of T2, b₂ is Element of bool the carrier of T1 : ( b₁ in the topology of T2 & b₂ in the topology of T1 ) } is set
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₁) where b₁ is Element of bool (bool the carrier of [:T2,T1:]) : b₁ c= { [:b₁,b₂:] where b₂ is Element of bool the carrier of T2, b₃ is Element of bool the carrier of T1 : ( b₁ in the topology of T2 & b₂ in the topology of T1 ) } } is set
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₁ where b₁ is open Element of bool the carrier of T1 : [:([#] T2),b₁:] c= union (Base-Appr ([#] [:T2,T1:])) } is set
[#] 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₁ where b₁ is Element of the carrier of T1 : [:([#] T2),{b₁}:] c= union S2 } is set
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₁ where b₁ is open Element of bool the carrier of T1 : ex b₂ being Element of bool (bool the carrier of [:T2,T1:]) st
( b₂ c= S2 & b₂ is finite & [:([#] T2),b₁:] c= union b₂ ) } is set
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₁ where b₁ is Element of the carrier of T1 : [:([#] T2),{b₁}:] c= union S1 } is set
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₁ where b₁ is open Element of bool the carrier of T1 : ex b₂ being Element of bool (bool the carrier of [:T2,T1:]) st
( b₂ c= S2 & b₂ is finite & [:([#] T2),b₁:] c= union b₂ ) } is set
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₁ where b₁ is open Element of bool the carrier of T1 : ex b₂ being Element of bool (bool the carrier of [:T2,T1:]) st
( b₂ c= S1 & b₂ is finite & [:([#] T2),b₁:] c= union b₂ ) } is set
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₁(b₁) where b₁ is Element of bool the carrier of T1 : b₁ in S2 } is set
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 set
{s} is non empty trivial set
{{s,A1},{s}} is non empty set
A1 is set
X1 is open Element of bool the carrier of T1
[:([#] T2),X1:] is 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
[:([#] T2),([#] T1):] is non empty 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:]
union (union (rng A)) is set
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 open Element of bool the carrier of T1
[:([#] T2),A1:] is Element of bool the carrier of [:T2,T1:]
A . A1 is set
X1 is Element of bool (bool the carrier of [:T2,T1:])
union X1 is Element of bool the carrier of [:T2,T1:]
Y1 is set
AA is set
s is set
A . s is set
[:([#] T2),s:] is set
A1 is Element of bool (bool the carrier of [:T2,T1:])
union A1 is Element of bool the carrier of [:T2,T1:]
T1 is non empty TopSpace-like compact TopStruct
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
bool (bool the carrier of [:T1,T2:]) is non empty set
S2 is Element of bool (bool the carrier of [:T1,T2:])
T1 is TopSpace-like compact TopStruct
T2 is TopSpace-like compact TopStruct
[:T1,T2:] is strict TopSpace-like TopStruct
T1 is TopSpace-like TopStruct
T2 is TopSpace-like TopStruct
[:T1,T2:] is strict TopSpace-like TopStruct
S1 is TopSpace-like SubSpace of T1
[:S1,T2:] is strict TopSpace-like TopStruct
the carrier of [:S1,T2:] is set
the carrier of S1 is set
the carrier of T2 is set
[: the carrier of S1, the carrier of T2:] is set
the carrier of [:T1,T2:] is set
the carrier of T1 is set
[: the carrier of T1, the carrier of T2:] is set
bool the carrier of [:S1,T2:] is non empty set
the topology of [:S1,T2:] is non empty open Element of bool (bool the carrier of [:S1,T2:])
bool (bool the carrier of [:S1,T2:]) is non empty set
bool the carrier of [:T1,T2:] is non empty set
the topology of [:T1,T2:] is non empty open Element of bool (bool the carrier of [:T1,T2:])
bool (bool the carrier of [:T1,T2:]) is non empty set
[#] [:S1,T2:] is non proper open closed dense Element of bool the carrier of [:S1,T2:]
S2 is Element of bool the carrier of [:S1,T2:]
S1 is Element of bool the carrier of [:S1,T2:]
bool the carrier of S1 is non empty set
bool the carrier of T2 is non empty set
X is Element of bool (bool the carrier of [:S1,T2:])
union X is Element of bool the carrier of [:S1,T2:]
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₂:] where b₁ is Element of bool the carrier of T1, b₂ is Element of bool the carrier of T2 : ex b₃ being Element of bool the carrier of S1 st
( b₃ = b₁ /\ ([#] S1) & b₁ is open & b₂ is open & [:b₃,b₂:] in X ) } is set
bool the carrier of [:T1,T2:] is non empty Element of bool (bool the carrier of [:T1,T2:])
A is set
A is Element of bool the carrier of T1
AA is Element of bool the carrier of T2
[:A,AA:] is Element of bool the carrier of [:T1,T2:]
AA is Element of bool the carrier of S1
A /\ ([#] S1) is Element of bool the carrier of S1
[:AA,AA:] is Element of bool the carrier of [:S1,T2:]
A is Element of bool (bool the carrier of [:T1,T2:])
A is Element of bool (bool the carrier of [:T1,T2:])
union A is Element of bool the carrier of [:T1,T2:]
(union A) /\ ([#] [:S1,T2:]) is Element of bool the carrier of [:S1,T2:]
AA is set
AA is set
AA is Element of bool the carrier of [:S1,T2:]
s is Element of bool the carrier of S1
A1 is Element of bool the carrier of T2
[:s,A1:] is Element of bool the carrier of [:S1,T2:]
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
[:D2,A1:] is Element of bool the carrier of [:T1,T2:]
AA is set
{AA} is non empty trivial set
AA is Element of bool the carrier of T1
s is Element of bool the carrier of T2
[:AA,s:] is Element of bool the carrier of [:T1,T2:]
AA /\ ([#] S1) is Element of bool the carrier of S1
A1 is set
A1 is Element of bool (bool the carrier of [:T1,T2:])
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
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
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of T1, b₂ is Element of bool the carrier of T2 : ( b₁ in the topology of T1 & b₂ in the topology of T2 ) } is set
A1 is set
X1 is Element of bool the carrier of S1
[:X1,s:] is Element of bool the carrier of [:S1,T2:]
union A1 is Element of bool the carrier of [:T1,T2:]
{ (union b₁) where b₁ is Element of bool (bool the carrier of [:T1,T2:]) : b₁ c= { [:b₁,b₂:] where b₂ is Element of bool the carrier of T1, b₃ is Element of bool the carrier of T2 : ( b₁ in the topology of T1 & b₂ in the topology of T2 ) } } is set
AA is set
AA is set
AA is Element of bool the carrier of T1
s is Element of bool the carrier of T2
[:AA,s:] is Element of bool the carrier of [:T1,T2:]
AA /\ ([#] S1) is Element of bool the carrier of S1
A1 is Element of bool the carrier of S1
[:A1,s:] is Element of bool the carrier of [:S1,T2:]
A1 is Element of bool the carrier of S1
[:A1,s:] is Element of bool the carrier of [:S1,T2:]
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 [:T1,T2:]
X /\ ([#] [:S1,T2:]) is Element of bool the carrier of [:S1,T2:]
Q9 is Element of bool the carrier of [:T1,T2:]
A is Element of bool (bool the carrier of [:T1,T2:])
union A is Element of bool the carrier of [:T1,T2:]
T2 is Element of bool the carrier of [:T1,T2:]
[:T1,T2:] | T2 is strict TopSpace-like SubSpace of [:T1,T2:]
the carrier of ([:T1,T2:] | T2) is set
bool the carrier of ([:T1,T2:] | T2) is non empty set
bool (bool the carrier of ([:T1,T2:] | T2)) is non empty set
A is Element of bool (bool the carrier of [:T1,T2:])
A | T2 is Element of bool (bool the carrier of ([:T1,T2:] | T2))
AA is Element of bool (bool the carrier of ([:T1,T2:] | T2))
AA is Element of bool (bool the carrier of [:S1,T2:])
AA is Element of bool (bool the carrier of [:S1,T2:])
s is set
A1 is Element of bool the carrier of ([:T1,T2:] | T2)
A1 is Element of bool the carrier of [:T1,T2:]
A1 /\ T2 is Element of bool the carrier of [:T1,T2:]
X1 is Element of bool the carrier of T1
Y1 is Element of bool the carrier of T2
[:X1,Y1:] is Element of bool the carrier of [:T1,T2:]
X1 /\ ([#] 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
[:([#] S1),([#] T2):] is Element of bool the carrier of [:S1,T2:]
Y1 /\ ([#] T2) is Element of bool the carrier of T2
[:(X1 /\ ([#] S1)),(Y1 /\ ([#] T2)):] is Element of bool the carrier of [:S1,T2:]
union A is Element of bool the carrier of [:T1,T2:]
(union A) /\ T2 is Element of bool the carrier of [:T1,T2:]
union AA is Element of bool the carrier of [:S1,T2:]
s is set
A1 is set
A1 /\ T2 is Element of bool the carrier of [:T1,T2:]
A1 is Element of bool the carrier of [:T1,T2:]
A1 /\ T2 is Element of bool the carrier of [:T1,T2:]
[#] [:T1,T2:] is non proper open closed dense Element of bool the carrier of [:T1,T2:]
T1 is TopSpace-like TopStruct
T2 is TopSpace-like TopStruct
[:T1,T2:] is strict TopSpace-like TopStruct
S1 is TopSpace-like SubSpace of T1
S2 is TopSpace-like SubSpace of T2
[:S1,S2:] is strict TopSpace-like TopStruct
[:S1,T2:] is strict TopSpace-like TopStruct
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
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
T1 | S2 is strict TopSpace-like SubSpace of T1
S2 is Element of bool the carrier of T2
[:S2,S2:] is Element of bool the carrier of [:T2,T1:]
T2 | S2 is strict TopSpace-like SubSpace of T2
[:(T2 | S2),(T1 | S2):] is strict TopSpace-like TopStruct
the carrier of [:(T2 | S2),(T1 | S2):] is set
the topology of [:(T2 | S2),(T1 | S2):] is non empty open Element of bool (bool the carrier of [:(T2 | S2),(T1 | S2):])
bool the carrier of [:(T2 | S2),(T1 | S2):] is non empty set
bool (bool the carrier of [:(T2 | S2),(T1 | S2):]) is non empty set
TopStruct(# the carrier of [:(T2 | S2),(T1 | S2):], the topology of [:(T2 | S2),(T1 | S2):] #) is strict TopSpace-like TopStruct
T2 is TopSpace-like SubSpace of [:T2,T1:]
the carrier of T2 is set
the carrier of (T2 | S2) is set
the carrier of (T1 | S2) is set
[: the carrier of (T2 | S2), the carrier of (T1 | S2):] is set
[: the carrier of (T2 | S2),S2:] is set
T1 is TopSpace-like TopStruct
the carrier of T1 is set
bool the carrier of T1 is non empty set
{} T1 is empty trivial open closed boundary nowhere_dense compact Element of bool the carrier of T1
T1 is TopSpace-like TopStruct
the carrier of T1 is set
bool the carrier of T1 is non empty set
T2 is compact Element of bool the carrier of T1
T1 | T2 is strict TopSpace-like SubSpace of T1
T1 is TopSpace-like TopStruct
the carrier of T1 is set
bool the carrier of T1 is non empty set
T2 is TopSpace-like TopStruct
the carrier of T2 is set
bool the carrier of T2 is non empty set
[:T1,T2:] is strict TopSpace-like TopStruct
the carrier of [:T1,T2:] is set
bool the carrier of [:T1,T2:] is non empty set
S1 is Element of bool the carrier of T1
S2 is Element of bool the carrier of T2
[:S1,S2:] is Element of bool the carrier of [:T1,T2:]
S2 is set
S1 is set
T2 is non empty TopSpace-like TopStruct
the carrier of T2 is non empty set
bool the carrier of T2 is non empty set
S2 is non empty TopSpace-like TopStruct
the carrier of S2 is non empty set
bool the carrier of S2 is non empty set
[:S2,T2:] is non empty strict TopSpace-like TopStruct
the carrier of [:S2,T2:] is non empty set
bool the carrier of [:S2,T2:] is non empty set
S1 is non empty compact Element of bool the carrier of S2
S2 is non empty compact Element of bool the carrier of T2
[:S1,S2:] is non empty Element of bool the carrier of [:S2,T2:]
S2 | S1 is non empty strict TopSpace-like compact SubSpace of S2
T2 | S2 is non empty strict TopSpace-like compact SubSpace of T2
[:(S2 | S1),(T2 | S2):] is non empty strict TopSpace-like compact TopStruct
the carrier of [:(S2 | S1),(T2 | S2):] is non empty set
the topology of [:(S2 | S1),(T2 | S2):] is non empty open Element of bool (bool the carrier of [:(S2 | S1),(T2 | S2):])
bool the carrier of [:(S2 | S1),(T2 | S2):] is non empty set
bool (bool the carrier of [:(S2 | S1),(T2 | S2):]) is non empty set
TopStruct(# the carrier of [:(S2 | S1),(T2 | S2):], the topology of [:(S2 | S1),(T2 | S2):] #) is non empty strict TopSpace-like TopStruct
X is Element of bool the carrier of [:S2,T2:]
[:S2,T2:] | X is strict TopSpace-like SubSpace of [:S2,T2:]
the carrier of ([:S2,T2:] | X) is set
the topology of ([:S2,T2:] | X) is non empty open Element of bool (bool the carrier of ([:S2,T2:] | X))
bool the carrier of ([:S2,T2:] | X) is non empty set
bool (bool the carrier of ([:S2,T2:] | X)) is non empty set
TopStruct(# the carrier of ([:S2,T2:] | X), the topology of ([:S2,T2:] | X) #) is strict TopSpace-like TopStruct
S2 is empty trivial open closed boundary nowhere_dense compact Element of bool the carrier of T1
[:S2,S2:] is empty trivial open closed boundary nowhere_dense compact Element of bool the carrier of [:T1,T2:]
{} [:T1,T2:] is empty trivial open closed boundary nowhere_dense compact Element of bool the carrier of [:T1,T2:]
S2 is empty trivial open closed boundary nowhere_dense compact Element of bool the carrier of T2
[:S1,S2:] is empty trivial open closed boundary nowhere_dense compact Element of bool the carrier of [:T1,T2:]
{} [:T1,T2:] is empty trivial open closed boundary nowhere_dense compact Element of bool the carrier of [:T1,T2:]
S2 is empty trivial open closed boundary nowhere_dense compact Element of bool the carrier of T2
[:S1,S2:] is empty trivial open closed boundary nowhere_dense compact Element of bool the carrier of [:T1,T2:]
{} [:T1,T2:] is empty trivial open closed boundary nowhere_dense compact Element of bool the carrier of [:T1,T2:]