:: TOPALG_3 semantic presentation

K28() is V192() V193() V194() V198() set

K32() is V192() V193() V194() V195() V196() V197() V198() Element of bool K28()

bool K28() is non empty set

K527() is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected SubSpace of K525()

K525() is non empty strict TopSpace-like V255() TopStruct

the carrier of K527() is non empty V192() V193() V194() set

[:K527(),K527():] is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of [:K527(),K527():] is non empty set

K27() is V192() V193() V194() V195() V196() V197() V198() set

bool K27() is non empty set

bool K32() is non empty set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() set

1 is non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() Element of K32()

{{},1} is non empty set

[:1,1:] is non empty Relation-like set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is non empty Relation-like set

bool [:[:1,1:],1:] is non empty set

[:[:1,1:],K28():] is Relation-like set

bool [:[:1,1:],K28():] is non empty set

[:K28(),K28():] is Relation-like set

[:[:K28(),K28():],K28():] is Relation-like set

bool [:[:K28(),K28():],K28():] is non empty set

2 is non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() Element of K32()

[:2,2:] is non empty Relation-like set

[:[:2,2:],K28():] is Relation-like set

bool [:[:2,2:],K28():] is non empty set

K29() is V192() V198() set

K30() is V192() V193() V194() V195() V198() set

K31() is V192() V193() V194() V195() V196() V198() set

bool [:K28(),K28():] is non empty set

TOP-REAL 2 is non empty TopSpace-like V89() V117() V118() V119() V120() V121() V122() V123() V207() L18()

the carrier of (TOP-REAL 2) is non empty set

bool the carrier of (TOP-REAL 2) is non empty set

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected TopStruct

the carrier of I[01] is non empty V192() V193() V194() set

K333() is V170() V255() L17()

[: the carrier of K527(), the carrier of K527():] is non empty Relation-like set

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

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

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

the carrier of [:I[01],I[01]:] is non empty set

0[01] is V11() V12() ext-real Element of the carrier of I[01]

0 is empty V10() V11() V12() Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real V168() V169() V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of K32()

1[01] is V11() V12() ext-real Element of the carrier of I[01]

K52(1,2) is V11() V12() ext-real Element of K28()

[: the carrier of I[01], the carrier of I[01]:] is non empty Relation-like set

S is set

T is set

[:S,T:] is Relation-like set

bool [:S,T:] is non empty set

s is set

t is set

s .--> t is Relation-like {s} -defined Function-like one-to-one set

{s} is non empty set

{s} --> t is non empty Relation-like {s} -defined {t} -valued Function-like constant V26({s}) quasi_total Element of bool [:{s},{t}:]

{t} is non empty set

[:{s},{t}:] is non empty Relation-like set

bool [:{s},{t}:] is non empty set

f is Relation-like S -defined T -valued Function-like quasi_total Element of bool [:S,T:]

f +* (s .--> t) is Relation-like Function-like set

rng (s .--> t) is set

rng (f +* (s .--> t)) is set

rng f is Element of bool T

bool T is non empty set

(rng f) \/ (rng (s .--> t)) is set

T \/ T is set

dom (f +* (s .--> t)) is set

dom f is Element of bool S

bool S is non empty set

dom (s .--> t) is Element of bool {s}

bool {s} is non empty set

(dom f) \/ (dom (s .--> t)) is set

S \/ (dom (s .--> t)) is set

S \/ {s} is non empty set

S is Relation-like Function-like set

T is set

S | T is Relation-like Function-like set

s is set

rng (S | T) is set

(S | T) " is Relation-like Function-like set

((S | T) ") * S is Relation-like Function-like set

(((S | T) ") * S) . s is set

dom (S | T) is set

f is set

(S | T) . f is set

dom S is set

(dom S) /\ T is set

dom ((S | T) ") is set

((S | T) ") . s is set

S . (((S | T) ") . s) is set

S . f is set

S is set

T is set

s is set

{T,s} is non empty set

[:S,{T,s}:] is Relation-like set

bool [:S,{T,s}:] is non empty set

{T} is non empty set

{s} is non empty set

t is Relation-like S -defined {T,s} -valued Function-like V26(S) quasi_total Element of bool [:S,{T,s}:]

t " {T} is Element of bool S

bool S is non empty set

t " {s} is Element of bool S

(t " {T}) \/ (t " {s}) is Element of bool S

t " {T,s} is Element of bool S

{T} \/ {s} is non empty set

t " ({T} \/ {s}) is Element of bool S

S is non empty 1-sorted

the carrier of S is non empty set

T is non empty 1-sorted

the carrier of T is non empty set

t is Element of the carrier of T

S --> t is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

the carrier of S --> t is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like constant V26( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

{t} is non empty set

[: the carrier of S,{t}:] is non empty Relation-like set

s is Element of the carrier of S

(S --> t) . s is Element of the carrier of T

S is non empty TopStruct

the carrier of S is non empty set

bool the carrier of S is non empty set

T is Element of the carrier of S

{T} is non empty set

Sspace T is non empty strict SubSpace of S

s is Element of bool the carrier of S

S | s is strict SubSpace of S

the carrier of (Sspace T) is non empty set

[#] (S | s) is non proper Element of bool the carrier of (S | s)

the carrier of (S | s) is set

bool the carrier of (S | s) is non empty set

S is TopSpace-like TopStruct

the carrier of S is set

bool the carrier of S is non empty set

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

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

TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of S, the topology of S #) is set

bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set

T is Element of bool the carrier of S

s is Element of bool the carrier of S

t is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

f is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

Cl T is closed Element of bool the carrier of S

Cl t is closed Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

Cl s is closed Element of bool the carrier of S

Cl f is closed Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

{0,1} is non empty V192() V193() V194() V195() V196() V197() set

1TopSp {0,1} is non empty strict TopSpace-like V156() TopStruct

the carrier of (1TopSp {0,1}) is non empty set

{0} is non empty functional V192() V193() V194() V195() V196() V197() set

{1} is non empty V192() V193() V194() V195() V196() V197() set

t is non empty TopSpace-like TopStruct

the carrier of t is non empty set

[: the carrier of t, the carrier of (1TopSp {0,1}):] is non empty Relation-like set

bool [: the carrier of t, the carrier of (1TopSp {0,1}):] is non empty set

bool the carrier of (1TopSp {0,1}) is non empty set

[#] t is non empty non proper open closed Element of bool the carrier of t

bool the carrier of t is non empty set

P is non empty Relation-like the carrier of t -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of t) quasi_total Element of bool [: the carrier of t, the carrier of (1TopSp {0,1}):]

f is non empty open Element of bool the carrier of (1TopSp {0,1})

P " f is Element of bool the carrier of t

f is non empty open Element of bool the carrier of (1TopSp {0,1})

P " f is Element of bool the carrier of t

rng P is non empty Element of bool the carrier of (1TopSp {0,1})

{} t is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of t

(P " f) \/ (P " f) is Element of bool the carrier of t

[#] (1TopSp {0,1}) is non empty non proper open closed Element of bool the carrier of (1TopSp {0,1})

c

P is Element of the carrier of (1TopSp {0,1})

{} t is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of t

x2 is Element of bool the carrier of t

ls1 is Element of bool the carrier of t

x2 \/ ls1 is Element of bool the carrier of t

ls2 is set

ls2 is non empty Relation-like the carrier of t -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of t) quasi_total Element of bool [: the carrier of t, the carrier of (1TopSp {0,1}):]

a1 is non empty Relation-like the carrier of t -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of t) quasi_total Element of bool [: the carrier of t, the carrier of (1TopSp {0,1}):]

dom a1 is non empty Element of bool the carrier of t

f is non empty open Element of bool the carrier of (1TopSp {0,1})

a1 " f is Element of bool the carrier of t

a2 is set

a1 . a2 is set

a2 is set

a1 . a2 is set

f is non empty open Element of bool the carrier of (1TopSp {0,1})

a1 " f is Element of bool the carrier of t

a2 is set

a1 . a2 is set

a2 is set

a1 . a2 is set

rng a1 is non empty Element of bool the carrier of (1TopSp {0,1})

a2 is set

P2 is set

a1 . P2 is set

P2 is set

a1 . P2 is set

{} (1TopSp {0,1}) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of (1TopSp {0,1})

a1 " ({} (1TopSp {0,1})) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of t

[#] (1TopSp {0,1}) is non empty non proper open closed Element of bool the carrier of (1TopSp {0,1})

a1 " ([#] (1TopSp {0,1})) is Element of bool the carrier of t

a2 is Element of bool the carrier of (1TopSp {0,1})

a1 " a2 is Element of bool the carrier of t

S is TopStruct

the carrier of S is set

bool the carrier of S is non empty set

[#] S is non proper Element of bool the carrier of S

T is Element of bool the carrier of S

{} S is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of S

s is empty trivial V45() {} -element T_0 T_1 T_2 TopStruct

the carrier of s is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V30() V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() set

t is Element of bool the carrier of S

T \/ t is Element of bool the carrier of S

S is TopSpace-like TopStruct

the carrier of S is set

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

bool the carrier of S is non empty set

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

TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

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

s is Element of bool the carrier of S

t is Element of bool the carrier of S

s \/ t is Element of bool the carrier of S

{} S is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of S

the carrier of TopStruct(# the carrier of S, the topology of S #) is set

bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set

[#] TopStruct(# the carrier of S, the topology of S #) is non proper open closed Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

f is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

f is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

f \/ f is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

{} TopStruct(# the carrier of S, the topology of S #) is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

S is TopSpace-like connected TopStruct

the carrier of S is set

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

bool the carrier of S is non empty set

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

TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of S, the topology of S #) is set

bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set

[#] TopStruct(# the carrier of S, the topology of S #) is non proper open closed Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

s is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

t is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

s \/ t is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

{} TopStruct(# the carrier of S, the topology of S #) is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

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

f is Element of bool the carrier of S

f is Element of bool the carrier of S

f \/ f is Element of bool the carrier of S

{} S is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of S

S is non empty TopSpace-like TopStruct

T is non empty TopSpace-like TopStruct

the carrier of S is non empty set

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

s is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

t is Element of the carrier of T

f is Element of the carrier of T

s " is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V26( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]

[: the carrier of T, the carrier of S:] is non empty Relation-like set

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

(s ") . t is Element of the carrier of S

(s ") . f is Element of the carrier of S

[: the carrier of I[01], the carrier of S:] is non empty Relation-like set

bool [: the carrier of I[01], the carrier of S:] is non empty set

f is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of S:]

f . 0 is set

f . 1 is set

[: the carrier of I[01], the carrier of T:] is non empty Relation-like set

bool [: the carrier of I[01], the carrier of T:] is non empty set

s * f is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of T:]

P is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of T:]

P . 0 is set

P . 1 is set

rng s is non empty Element of bool the carrier of T

bool the carrier of T is non empty set

[#] T is non empty non proper open closed Element of bool the carrier of T

s . ((s ") . t) is Element of the carrier of T

s * (s ") is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like V26( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

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

(s * (s ")) . t is Element of the carrier of T

id T is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like V26( the carrier of T) quasi_total continuous V247(T,T) Element of bool [: the carrier of T, the carrier of T:]

id the carrier of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one V26( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]

(id T) . t is Element of the carrier of T

s . ((s ") . f) is Element of the carrier of T

(s * (s ")) . f is Element of the carrier of T

(id T) . f is Element of the carrier of T

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is Element of the carrier of S

s is Element of the carrier of S

[: the carrier of I[01], the carrier of S:] is non empty Relation-like set

bool [: the carrier of I[01], the carrier of S:] is non empty set

I[01] --> T is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like V26( the carrier of I[01]) quasi_total continuous Element of bool [: the carrier of I[01], the carrier of S:]

the carrier of I[01] --> T is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like constant V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of S:]

{T} is non empty set

[: the carrier of I[01],{T}:] is non empty Relation-like set

t is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like V26( the carrier of I[01]) quasi_total continuous Element of bool [: the carrier of I[01], the carrier of S:]

t . 0 is set

t . 1 is set

S is TopSpace-like SubSpace of TOP-REAL 2

the carrier of S is set

s is Element of the carrier of S

t is Element of the carrier of S

T is non empty compact being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)

f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)

f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)

{f,f} is non empty set

P is non empty Element of bool the carrier of (TOP-REAL 2)

c

P \/ c

P /\ c

(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | P) is non empty set

[: the carrier of I[01], the carrier of ((TOP-REAL 2) | P):] is non empty Relation-like set

bool [: the carrier of I[01], the carrier of ((TOP-REAL 2) | P):] is non empty set

x2 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL 2) | P):]

x2 . 0 is set

x2 . 1 is set

[: the carrier of I[01], the carrier of S:] is Relation-like set

bool [: the carrier of I[01], the carrier of S:] is non empty set

ls1 is Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of I[01], the carrier of S:]

ls1 . 0 is set

ls1 . 1 is set

f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)

f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)

P is non empty TopSpace-like SubSpace of TOP-REAL 2

the carrier of P is non empty set

[: the carrier of I[01], the carrier of S:] is Relation-like set

bool [: the carrier of I[01], the carrier of S:] is non empty set

c

I[01] --> c

[: the carrier of I[01], the carrier of P:] is non empty Relation-like set

bool [: the carrier of I[01], the carrier of P:] is non empty set

the carrier of I[01] --> c

{c

[: the carrier of I[01],{c

x2 is Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of I[01], the carrier of S:]

x2 . 0 is set

x2 . 1 is set

j0 is V11() V12() ext-real Element of the carrier of I[01]

x2 . j0 is Element of the carrier of S

j1 is V11() V12() ext-real Element of the carrier of I[01]

x2 . j1 is Element of the carrier of S

f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)

f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)

S is TopSpace-like TopStruct

the carrier of S is set

bool the carrier of S is non empty set

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

{ the carrier of S} is non empty set

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

s is set

s is Element of bool (bool the carrier of S)

union s is Element of bool the carrier of S

t is Element of bool the carrier of S

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

S is TopSpace-like TopStruct

the carrier of S is set

bool the carrier of S is non empty set

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

{} S is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of S

{({} S)} is non empty functional set

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

s is set

s is Element of bool (bool the carrier of S)

t is Element of bool the carrier of S

t is Element of bool the carrier of S

S is TopSpace-like TopStruct

the carrier of S is set

bool the carrier of S is non empty set

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

T is open mutually-disjoint Element of bool (bool the carrier of S)

s is Element of bool the carrier of S

t is set

S | s is strict TopSpace-like SubSpace of S

f is set

union T is Element of bool the carrier of S

f is set

P is set

{ (b

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

bool s is non empty set

bool (bool s) is non empty set

x2 is set

ls1 is Element of bool the carrier of S

ls1 /\ s is Element of bool the carrier of S

the carrier of (S | s) is set

bool the carrier of (S | s) is non empty set

bool (bool the carrier of (S | s)) is non empty set

t /\ s is Element of bool the carrier of S

x2 is Element of bool (bool the carrier of (S | s))

union x2 is Element of bool the carrier of (S | s)

{ (b

ls2 is set

a1 is Element of bool the carrier of S

a1 /\ s is Element of bool the carrier of S

ls2 is Element of bool (bool the carrier of (S | s))

union ls2 is Element of bool the carrier of (S | s)

(union ls2) \/ (union x2) is Element of bool the carrier of (S | s)

a1 is set

a2 is set

P2 is Element of bool the carrier of S

P2 /\ s is Element of bool the carrier of S

P /\ s is Element of bool the carrier of S

[#] (S | s) is non proper open closed Element of bool the carrier of (S | s)

a1 is Element of bool the carrier of (S | s)

a2 is Element of bool the carrier of S

a2 /\ s is Element of bool the carrier of S

a1 is Element of bool the carrier of (S | s)

a2 is Element of bool the carrier of S

a2 /\ s is Element of bool the carrier of S

{} (S | s) is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of (S | s)

a1 is set

a2 is set

P2 is Element of bool the carrier of S

P2 /\ s is Element of bool the carrier of S

P1 is set

M is Element of bool the carrier of S

M /\ s is Element of bool the carrier of S

S is TopSpace-like TopStruct

T is TopSpace-like TopStruct

[:S,T:] is strict TopSpace-like TopStruct

the carrier of [:S,T:] is set

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

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

bool (bool the carrier of [:S,T:]) is non empty set

TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) is strict TopSpace-like TopStruct

the carrier of S is set

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

bool the carrier of S is non empty set

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

TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

the carrier of T is set

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

bool the carrier of T is non empty set

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

TopStruct(# the carrier of T, the topology of T #) is strict TopSpace-like TopStruct

[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct

[: the carrier of S, the carrier of T:] is Relation-like set

the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is set

bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is non empty set

s is Element of bool the carrier of [:S,T:]

t is Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]

f is Element of bool (bool the carrier of [:S,T:])

union f is Element of bool the carrier of [:S,T:]

bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]) is non empty set

f is Element of bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):])

the carrier of TopStruct(# the carrier of S, the topology of S #) is set

bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set

the carrier of TopStruct(# the carrier of T, the topology of T #) is set

bool the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set

P is set

c

x2 is Element of bool the carrier of T

[:c

ls2 is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

ls1 is Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #)

[:ls2,ls1:] is Relation-like Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]

f is Element of bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):])

union f is Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]

f is Element of bool (bool the carrier of [:S,T:])

P is set

c

x2 is Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #)

[:c

ls2 is Element of bool the carrier of S

ls1 is Element of bool the carrier of T

[:ls2,ls1:] is Relation-like Element of bool the carrier of [:S,T:]

S is TopSpace-like TopStruct

the carrier of S is set

bool the carrier of S is non empty set

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

[:S,T:] is strict TopSpace-like TopStruct

s is Element of bool the carrier of S

Cl s is closed Element of bool the carrier of S

t is Element of bool the carrier of T

[:s,t:] is Relation-like Element of bool the carrier of [:S,T:]

the carrier of [:S,T:] is set

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

Cl [:s,t:] is closed Element of bool the carrier of [:S,T:]

Cl t is closed Element of bool the carrier of T

[:(Cl s),(Cl t):] is Relation-like Element of bool the carrier of [:S,T:]

f is set

f is non empty TopSpace-like TopStruct

P is non empty TopSpace-like TopStruct

[:f,P:] is non empty strict TopSpace-like TopStruct

the carrier of [:f,P:] is non empty set

c

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

bool (bool the carrier of [:f,P:]) is non empty set

x2 is open V218([:f,P:],c

the carrier of f is non empty set

the carrier of P is non empty set

ls1 is Element of the carrier of f

ls2 is Element of the carrier of P

[ls1,ls2] is Element of the carrier of [:f,P:]

{ls1,ls2} is non empty set

{ls1} is non empty set

{{ls1,ls2},{ls1}} is non empty set

bool the carrier of P is non empty set

a1 is Element of bool the carrier of P

[#] f is non empty non proper open closed Element of bool the carrier of f

bool the carrier of f is non empty set

[:([#] f),a1:] is Relation-like Element of bool the carrier of [:f,P:]

a2 is Element of bool the carrier of [:f,P:]

P2 is set

[:s,t:] /\ [:([#] f),a1:] is Relation-like Element of bool the carrier of [:f,P:]

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

t /\ a1 is Element of bool the carrier of P

[:(s /\ ([#] f)),(t /\ a1):] is Relation-like Element of bool the carrier of [:f,P:]

P1 is set

M is set

[P1,M] is set

{P1,M} is non empty set

{P1} is non empty set

{{P1,M},{P1}} is non empty set

bool the carrier of f is non empty set

a1 is Element of bool the carrier of f

[#] P is non empty non proper open closed Element of bool the carrier of P

[:a1,([#] P):] is Relation-like Element of bool the carrier of [:f,P:]

a2 is Element of bool the carrier of [:f,P:]

P2 is set

[:s,t:] /\ [:a1,([#] P):] is Relation-like Element of bool the carrier of [:f,P:]

s /\ a1 is Element of bool the carrier of f

t /\ ([#] P) is Element of bool the carrier of P

[:(s /\ a1),(t /\ ([#] P)):] is Relation-like Element of bool the carrier of [:f,P:]

P1 is set

M is set

[P1,M] is set

{P1,M} is non empty set

{P1} is non empty set

{{P1,M},{P1}} is non empty set

f is set

f is set

P is set

[f,P] is set

{f,P} is non empty set

{f} is non empty set

{{f,P},{f}} is non empty set

c

the carrier of c

ls1 is Element of the carrier of c

bool the carrier of c

bool (bool the carrier of c

ls2 is open V218(c

x2 is non empty TopSpace-like TopStruct

the carrier of x2 is non empty set

a1 is Element of the carrier of x2

bool the carrier of x2 is non empty set

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

a2 is open V218(x2,a1) Element of bool (bool the carrier of x2)

[:c

the carrier of [:c

bool the carrier of [:c

[ls1,a1] is Element of the carrier of [:c

{ls1,a1} is non empty set

{ls1} is non empty set

{{ls1,a1},{ls1}} is non empty set

P2 is Element of bool the carrier of [:c

bool (bool the carrier of [:c

P1 is Element of bool (bool the carrier of [:c

union P1 is Element of bool the carrier of [:c

M is set

x0 is Element of bool the carrier of c

x1 is Element of bool the carrier of x2

[:x0,x1:] is Relation-like Element of bool the carrier of [:c

S is Element of bool the carrier of x2

T is set

Y1 is Element of bool the carrier of c

h is set

[h,T] is set

{h,T} is non empty set

{h} is non empty set

{{h,T},{h}} is non empty set

S is TopSpace-like TopStruct

the carrier of S is set

bool the carrier of S is non empty set

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

[:S,T:] is strict TopSpace-like TopStruct

s is closed Element of bool the carrier of S

t is closed Element of bool the carrier of T

[:s,t:] is Relation-like Element of bool the carrier of [:S,T:]

the carrier of [:S,T:] is set

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

Cl s is closed Element of bool the carrier of S

Cl [:s,t:] is closed Element of bool the carrier of [:S,T:]

Cl t is closed Element of bool the carrier of T

[:(Cl s),(Cl t):] is Relation-like Element of bool the carrier of [:S,T:]

S is TopSpace-like connected TopStruct

T is TopSpace-like connected TopStruct

[:S,T:] is strict TopSpace-like TopStruct

the carrier of S is set

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

bool the carrier of S is non empty set

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

TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like connected TopStruct

the carrier of T is set

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

bool the carrier of T is non empty set

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

TopStruct(# the carrier of T, the topology of T #) is strict TopSpace-like connected TopStruct

the carrier of [:S,T:] is set

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

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

bool (bool the carrier of [:S,T:]) is non empty set

TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) is strict TopSpace-like TopStruct

[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct

the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is set

[: the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):], the carrier of (1TopSp {0,1}):] is Relation-like set

bool [: the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):], the carrier of (1TopSp {0,1}):] is non empty set

f is Relation-like the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]) quasi_total Element of bool [: the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):], the carrier of (1TopSp {0,1}):]

rng f is Element of bool the carrier of (1TopSp {0,1})

bool the carrier of (1TopSp {0,1}) is non empty set

dom f is Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]

bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is non empty set

P is Element of the carrier of (1TopSp {0,1})

x2 is set

f . x2 is set

c

ls1 is set

f . ls1 is set

the carrier of TopStruct(# the carrier of S, the topology of S #) is set

the carrier of TopStruct(# the carrier of T, the topology of T #) is set

[: the carrier of TopStruct(# the carrier of S, the topology of S #), the carrier of TopStruct(# the carrier of T, the topology of T #):] is Relation-like set

ls2 is set

a1 is set

[ls2,a1] is set

{ls2,a1} is non empty set

{ls2} is non empty set

{{ls2,a1},{ls2}} is non empty set

a2 is set

P2 is set

[a2,P2] is set

{a2,P2} is non empty set

{a2} is non empty set

{{a2,P2},{a2}} is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

M is Element of the carrier of TopStruct(# the carrier of T, the topology of T #)

{M} is non empty set

S is non empty TopSpace-like TopStruct

[#] S is non empty non proper open closed Element of bool the carrier of S

the carrier of S is non empty set

bool the carrier of S is non empty set

Y1 is non empty Element of bool the carrier of T

[:([#] S),Y1:] is non empty Relation-like Element of bool the carrier of [:S,T:]

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

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

f | [:([#] S),Y1:] is Relation-like the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] -defined [:([#] S),Y1:] -defined the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] -defined the carrier of (1TopSp {0,1}) -valued Function-like Element of bool [: the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):], the carrier of (1TopSp {0,1}):]

dom (f | [:([#] S),Y1:]) is Relation-like [#] S -defined Y1 -valued Element of bool [:([#] S),Y1:]

bool [:([#] S),Y1:] is non empty set

T | Y1 is non empty strict TopSpace-like SubSpace of T

[:S,(T | Y1):] is non empty strict TopSpace-like TopStruct

the carrier of [:S,(T | Y1):] is non empty set

the carrier of (T | Y1) is non empty set

[: the carrier of S, the carrier of (T | Y1):] is non empty Relation-like set

rng (f | [:([#] S),Y1:]) is Element of bool the carrier of (1TopSp {0,1})

[: the carrier of [:S,(T | Y1):], the carrier of (1TopSp {0,1}):] is non empty Relation-like set

bool [: the carrier of [:S,(T | Y1):], the carrier of (1TopSp {0,1}):] is non empty set

[:(T | Y1),S:] is non empty strict TopSpace-like TopStruct

S | ([#] S) is non empty strict TopSpace-like SubSpace of S

[:(S | ([#] S)),(T | Y1):] is non empty strict TopSpace-like TopStruct

[:S,T:] | [:([#] S),Y1:] is non empty strict TopSpace-like SubSpace of [:S,T:]

h is non empty Relation-like the carrier of [:S,(T | Y1):] -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of [:S,(T | Y1):]) quasi_total Element of bool [: the carrier of [:S,(T | Y1):], the carrier of (1TopSp {0,1}):]

x0 is Element of the carrier of TopStruct(# the carrier of S, the topology of S #)

[x0,M] is set

{x0,M} is non empty set

{x0} is non empty set

{{x0,M},{x0}} is non empty set

f . [x0,M] is set

rng h is non empty Element of bool the carrier of (1TopSp {0,1})

X0 is set

x1 is Element of the carrier of TopStruct(# the carrier of S, the topology of S #)

[x1,M] is set

{x1,M} is non empty set

{x1} is non empty set

{{x1,M},{x1}} is non empty set

dom h is non empty Element of bool the carrier of [:S,(T | Y1):]

bool the carrier of [:S,(T | Y1):] is non empty set

h . [x1,M] is set

dom h is non empty Element of bool the carrier of [:S,(T | Y1):]

bool the carrier of [:S,(T | Y1):] is non empty set

h . [x0,M] is set

X0 is non empty Element of bool the carrier of S

[#] T is non empty non proper open closed Element of bool the carrier of T

[:X0,([#] T):] is non empty Relation-like Element of bool the carrier of [:S,T:]

f | [:X0,([#] T):] is Relation-like the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] -defined [:X0,([#] T):] -defined the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] -defined the carrier of (1TopSp {0,1}) -valued Function-like Element of bool [: the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):], the carrier of (1TopSp {0,1}):]

dom (f | [:X0,([#] T):]) is Relation-like X0 -defined [#] T -valued Element of bool [:X0,([#] T):]

bool [:X0,([#] T):] is non empty set

S | X0 is non empty strict TopSpace-like SubSpace of S

[:(S | X0),T:] is non empty strict TopSpace-like TopStruct

the carrier of [:(S | X0),T:] is non empty set

the carrier of (S | X0) is non empty set

[: the carrier of (S | X0), the carrier of T:] is non empty Relation-like set

rng (f | [:X0,([#] T):]) is Element of bool the carrier of (1TopSp {0,1})

[: the carrier of [:(S | X0),T:], the carrier of (1TopSp {0,1}):] is non empty Relation-like set

bool [: the carrier of [:(S | X0),T:], the carrier of (1TopSp {0,1}):] is non empty set

T | ([#] T) is non empty strict TopSpace-like SubSpace of T

[:(S | X0),(T | ([#] T)):] is non empty strict TopSpace-like TopStruct

[:S,T:] | [:X0,([#] T):] is non empty strict TopSpace-like SubSpace of [:S,T:]

g is non empty Relation-like the carrier of [:(S | X0),T:] -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of [:(S | X0),T:]) quasi_total Element of bool [: the carrier of [:(S | X0),T:], the carrier of (1TopSp {0,1}):]

rng g is non empty Element of bool the carrier of (1TopSp {0,1})

y is set

P1 is Element of the carrier of TopStruct(# the carrier of T, the topology of T #)

[x0,P1] is set

{x0,P1} is non empty set

{{x0,P1},{x0}} is non empty set

dom g is non empty Element of bool the carrier of [:(S | X0),T:]

bool the carrier of [:(S | X0),T:] is non empty set

g . [x0,P1] is set

dom g is non empty Element of bool the carrier of [:(S | X0),T:]

bool the carrier of [:(S | X0),T:] is non empty set

g . [x0,M] is set

S is TopSpace-like TopStruct

the carrier of S is set

bool the carrier of S is non empty set

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

[:S,T:] is strict TopSpace-like TopStruct

s is Element of bool the carrier of S

t is Element of bool the carrier of T

[:s,t:] is Relation-like Element of bool the carrier of [:S,T:]

the carrier of [:S,T:] is set

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

S | s is strict TopSpace-like SubSpace of S

T | t is strict TopSpace-like SubSpace of T

f is TopSpace-like connected TopStruct

f is TopSpace-like connected TopStruct

[:f,f:] is strict TopSpace-like connected TopStruct

[:S,T:] | [:s,t:] is strict TopSpace-like SubSpace of [:S,T:]

S is TopSpace-like TopStruct

the carrier of S is set

bool the carrier of S is non empty set

T is TopSpace-like TopStruct

[:S,T:] is strict TopSpace-like TopStruct

the carrier of [:S,T:] is set

the carrier of T is set

s is non empty TopSpace-like TopStruct

the carrier of s is non empty set

[: the carrier of [:S,T:], the carrier of s:] is Relation-like set

bool [: the carrier of [:S,T:], the carrier of s:] is non empty set

t is Element of bool the carrier of S

S | t is strict TopSpace-like SubSpace of S

[:(S | t),T:] is strict TopSpace-like TopStruct

the carrier of [:(S | t),T:] is set

[: the carrier of [:(S | t),T:], the carrier of s:] is Relation-like set

bool [: the carrier of [:(S | t),T:], the carrier of s:] is non empty set

[:t, the carrier of T:] is Relation-like set

f is Relation-like the carrier of [:S,T:] -defined the carrier of s -valued Function-like V26( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of s:]

f | [:t, the carrier of T:] is Relation-like the carrier of [:S,T:] -defined [:t, the carrier of T:] -defined the carrier of [:S,T:] -defined the carrier of s -valued Function-like Element of bool [: the carrier of [:S,T:], the carrier of s:]

f is Relation-like the carrier of [:(S | t),T:] -defined the carrier of s -valued Function-like V26( the carrier of [:(S | t),T:]) quasi_total Element of bool [: the carrier of [:(S | t),T:], the carrier of s:]

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

bool the carrier of T is non empty set

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

TopStruct(# the carrier of T, the topology of T #) is strict TopSpace-like TopStruct

[:(S | t),TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct

[#] TopStruct(# the carrier of T, the topology of T #) is non proper open closed Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #)

the carrier of TopStruct(# the carrier of T, the topology of T #) is set

bool the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set

TopStruct(# the carrier of T, the topology of T #) | ([#] TopStruct(# the carrier of T, the topology of T #)) is strict TopSpace-like SubSpace of TopStruct(# the carrier of T, the topology of T #)

[:(S | t),(TopStruct(# the carrier of T, the topology of T #) | ([#] TopStruct(# the carrier of T, the topology of T #))):] is strict TopSpace-like TopStruct

[:S,TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct

[:t,([#] TopStruct(# the carrier of T, the topology of T #)):] is Relation-like Element of bool the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):]

the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):] is set

bool the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):] is non empty set

[:S,TopStruct(# the carrier of T, the topology of T #):] | [:t,([#] TopStruct(# the carrier of T, the topology of T #)):] is strict TopSpace-like SubSpace of [:S,TopStruct(# the carrier of T, the topology of T #):]

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

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

bool (bool the carrier of [:S,T:]) is non empty set

TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) is strict TopSpace-like TopStruct

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

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

TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct

the topology of [:S,TopStruct(# the carrier of T, the topology of T #):] is non empty open Element of bool (bool the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):])

bool (bool the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):]) is non empty set

TopStruct(# the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):], the topology of [:S,TopStruct(# the carrier of T, the topology of T #):] #) is strict TopSpace-like TopStruct

the carrier of [:(S | t),TopStruct(# the carrier of T, the topology of T #):] is set

the topology of [:(S | t),TopStruct(# the carrier of T, the topology of T #):] is non empty open Element of bool (bool the carrier of [:(S | t),TopStruct(# the carrier of T, the topology of T #):])

bool the carrier of [:(S | t),TopStruct(# the carrier of T, the topology of T #):] is non empty set

bool (bool the carrier of [:(S | t),TopStruct(# the carrier of T, the topology of T #):]) is non empty set

TopStruct(# the carrier of [:(S | t),TopStruct(# the carrier of T, the topology of T #):], the topology of [:(S | t),TopStruct(# the carrier of T, the topology of T #):] #) is strict TopSpace-like TopStruct

the topology of [:(S | t),T:] is non empty open Element of bool (bool the carrier of [:(S | t),T:])

bool the carrier of [:(S | t),T:] is non empty set

bool (bool the carrier of [:(S | t),T:]) is non empty set

TopStruct(# the carrier of [:(S | t),T:], the topology of [:(S | t),T:] #) is strict TopSpace-like TopStruct

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

S is TopSpace-like TopStruct

[:S,T:] is strict TopSpace-like TopStruct

the carrier of [:S,T:] is set

the carrier of S is set

s is non empty TopSpace-like TopStruct

the carrier of s is non empty set

[: the carrier of [:S,T:], the carrier of s:] is Relation-like set

bool [: the carrier of [:S,T:], the carrier of s:] is non empty set

t is Element of bool the carrier of T

T | t is strict TopSpace-like SubSpace of T

[:S,(T | t):] is strict TopSpace-like TopStruct

the carrier of [:S,(T | t):] is set

[: the carrier of [:S,(T | t):], the carrier of s:] is Relation-like set

bool [: the carrier of [:S,(T | t):], the carrier of s:] is non empty set

[: the carrier of S,t:] is Relation-like set

f is Relation-like the carrier of [:S,T:] -defined the carrier of s -valued Function-like V26( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of s:]

f | [: the carrier of S,t:] is Relation-like the carrier of [:S,T:] -defined [: the carrier of S,t:] -defined the carrier of [:S,T:] -defined the carrier of s -valued Function-like Element of bool [: the carrier of [:S,T:], the carrier of s:]

f is Relation-like the carrier of [:S,(T | t):] -defined the carrier of s -valued Function-like V26( the carrier of [:S,(T | t):]) quasi_total Element of bool [: the carrier of [:S,(T | t):], the carrier of s:]

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

bool the carrier of S is non empty set

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

TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

[:TopStruct(# the carrier of S, the topology of S #),(T | t):] is strict TopSpace-like TopStruct

[#] TopStruct(# the carrier of S, the topology of S #) is non proper open closed Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)

the carrier of TopStruct(# the carrier of S, the topology of S #) is set

bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set

TopStruct(# the carrier of S, the topology of S #) | ([#] TopStruct(# the carrier of S, the topology of S #)) is strict TopSpace-like SubSpace of TopStruct(# the carrier of S, the topology of S #)

[:(TopStruct(# the carrier of S, the topology of S #) | ([#] TopStruct(# the carrier of S, the topology of S #))),(T | t):] is strict TopSpace-like TopStruct

[:TopStruct(# the carrier of S, the topology of S #),T:] is strict TopSpace-like TopStruct

[:([#] TopStruct(# the carrier of S, the topology of S #)),t:] is Relation-like Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:]

the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:] is set

bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:] is non empty set

[:TopStruct(# the carrier of S, the topology of S #),T:] | [:([#] TopStruct(# the carrier of S, the topology of S #)),t:] is strict TopSpace-like SubSpace of [:TopStruct(# the carrier of S, the topology of S #),T:]

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

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

bool (bool the carrier of [:S,T:]) is non empty set

TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) is strict TopSpace-like TopStruct

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

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

TopStruct(# the carrier of T, the topology of T #) is strict TopSpace-like TopStruct

[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct

the topology of [:TopStruct(# the carrier of S, the topology of S #),T:] is non empty open Element of bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:])

bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:]) is non empty set

TopStruct(# the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:], the topology of [:TopStruct(# the carrier of S, the topology of S #),T:] #) is strict TopSpace-like TopStruct

the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | t):] is set

the topology of [:TopStruct(# the carrier of S, the topology of S #),(T | t):] is non empty open Element of bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | t):])

bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | t):] is non empty set

bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | t):]) is non empty set

TopStruct(# the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | t):], the topology of [:TopStruct(# the carrier of S, the topology of S #),(T | t):] #) is strict TopSpace-like TopStruct

the topology of [:S,(T | t):] is non empty open Element of bool (bool the carrier of [:S,(T | t):])

bool the carrier of [:S,(T | t):] is non empty set

bool (bool the carrier of [:S,(T | t):]) is non empty set

TopStruct(# the carrier of [:S,(T | t):], the topology of [:S,(T | t):] #) is strict TopSpace-like TopStruct

f is non empty TopSpace-like TopStruct

s is non empty TopSpace-like TopStruct

[:f,s:] is non empty strict TopSpace-like TopStruct

the carrier of [:f,s:] is non empty set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

[: the carrier of [:f,s:], the carrier of S:] is non empty Relation-like set

bool [: the carrier of [:f,s:], the carrier of S:] is non empty set

t is non empty TopSpace-like TopStruct

[:f,t:] is non empty strict TopSpace-like TopStruct

the carrier of [:f,t:] is non empty set

[: the carrier of [:f,t:], the carrier of S:] is non empty Relation-like set

bool [: the carrier of [:f,t:], the carrier of S:] is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

[#] s is non empty non proper open closed Element of bool the carrier of s

the carrier of s is non empty set

bool the carrier of s is non empty set

[#] t is non empty non proper open closed Element of bool the carrier of t

the carrier of t is non empty set

bool the carrier of t is non empty set

([#] s) \/ ([#] t) is non empty set

[#] T is non empty non proper open closed Element of bool the carrier of T

[#] [:f,s:] is non empty non proper open closed Element of bool the carrier of [:f,s:]

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

[#] [:f,t:] is non empty non proper open closed Element of bool the carrier of [:f,t:]

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

([#] [:f,s:]) /\ ([#] [:f,t:]) is Element of bool the carrier of [:f,t:]

[:f,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:f,T:] is non empty set

[: the carrier of [:f,T:], the carrier of S:] is non empty Relation-like set

bool [: the carrier of [:f,T:], the carrier of S:] is non empty set

f is non empty Relation-like the carrier of [:f,s:] -defined the carrier of S -valued Function-like V26( the carrier of [:f,s:]) quasi_total Element of bool [: the carrier of [:f,s:], the carrier of S:]

P is non empty Relation-like the carrier of [:f,t:] -defined the carrier of S -valued Function-like V26( the carrier of [:f,t:]) quasi_total Element of bool [: the carrier of [:f,t:], the carrier of S:]

f +* P is Relation-like Function-like set

c

x2 is closed Element of bool the carrier of T

dom f is non empty Element of bool the carrier of [:f,s:]

the carrier of f is non empty set

[: the carrier of f, the carrier of t:] is non empty Relation-like set

rng (f +* P) is set

rng f is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

rng P is non empty Element of bool the carrier of S

(rng f) \/ (rng P) is non empty Element of bool the carrier of S

dom P is non empty Element of bool the carrier of [:f,t:]

dom (f +* P) is set

(dom f) \/ (dom P) is non empty set

[: the carrier of f, the carrier of s:] is non empty Relation-like set

[: the carrier of f, the carrier of T:] is non empty Relation-like set

ls2 is non empty Relation-like the carrier of [:f,T:] -defined the carrier of S -valued Function-like V26( the carrier of [:f,T:]) quasi_total Element of bool [: the carrier of [:f,T:], the carrier of S:]

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

[#] f is non empty non proper open closed Element of bool the carrier of f

bool the carrier of f is non empty set

[:([#] f),c

a2 is Element of bool the carrier of S

ls2 " a2 is Element of bool the carrier of [:f,T:]

P2 is set

(ls2 " a2) /\ ([#] [:f,t:]) is Element of bool the carrier of [:f,t:]

P " a2 is Element of bool the carrier of [:f,t:]

ls2 . P2 is set

P . P2 is set

P . P2 is set

ls2 . P2 is set

dom ls2 is non empty Element of bool the carrier of [:f,T:]

P2 is set

ls2 . P2 is set

f . P2 is set

P . P2 is set

P2 is set

(ls2 " a2) /\ ([#] [:f,s:]) is Element of bool the carrier of [:f,s:]

f " a2 is Element of bool the carrier of [:f,s:]

ls2 . P2 is set

f . P2 is set

f . P2 is set

ls2 . P2 is set

[#] [:f,T:] is non empty non proper open closed Element of bool the carrier of [:f,T:]

([#] [:f,s:]) \/ ([#] [:f,t:]) is non empty set

(ls2 " a2) /\ (([#] [:f,s:]) \/ ([#] [:f,t:])) is Element of bool the carrier of [:f,T:]

((ls2 " a2) /\ ([#] [:f,s:])) \/ ((ls2 " a2) /\ ([#] [:f,t:])) is set

(f " a2) \/ (P " a2) is set

a1 is Element of bool the carrier of [:f,T:]

P1 is Element of bool the carrier of [:f,T:]

M is Element of bool the carrier of [:f,T:]

M /\ ([#] [:f,s:]) is Element of bool the carrier of [:f,s:]

[:([#] f),x2:] is Relation-like Element of bool the carrier of [:f,T:]

M is Element of bool the carrier of [:f,T:]

P2 is Element of bool the carrier of [:f,T:]

x0 is Element of bool the carrier of [:f,T:]

x0 /\ ([#] [:f,t:]) is Element of bool the carrier of [:f,t:]

s is non empty TopSpace-like TopStruct

f is non empty TopSpace-like TopStruct

[:s,f:] is non empty strict TopSpace-like TopStruct

the carrier of [:s,f:] is non empty set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

[: the carrier of [:s,f:], the carrier of S:] is non empty Relation-like set

bool [: the carrier of [:s,f:], the carrier of S:] is non empty set

t is non empty TopSpace-like TopStruct

[:t,f:] is non empty strict TopSpace-like TopStruct

the carrier of [:t,f:] is non empty set

[: the carrier of [:t,f:], the carrier of S:] is non empty Relation-like set

bool [: the carrier of [:t,f:], the carrier of S:] is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

[#] s is non empty non proper open closed Element of bool the carrier of s

the carrier of s is non empty set

bool the carrier of s is non empty set

[#] t is non empty non proper open closed Element of bool the carrier of t

the carrier of t is non empty set

bool the carrier of t is non empty set

([#] s) \/ ([#] t) is non empty set

[#] T is non empty non proper open closed Element of bool the carrier of T

[#] [:s,f:] is non empty non proper open closed Element of bool the carrier of [:s,f:]

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

[#] [:t,f:] is non empty non proper open closed Element of bool the carrier of [:t,f:]

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

([#] [:s,f:]) /\ ([#] [:t,f:]) is Element of bool the carrier of [:t,f:]

[:T,f:] is non empty strict TopSpace-like TopStruct

the carrier of [:T,f:] is non empty set

[: the carrier of [:T,f:], the carrier of S:] is non empty Relation-like set

bool [: the carrier of [:T,f:], the carrier of S:] is non empty set

f is non empty Relation-like the carrier of [:s,f:] -defined the carrier of S -valued Function-like V26( the carrier of [:s,f:]) quasi_total Element of bool [: the carrier of [:s,f:], the carrier of S:]

P is non empty Relation-like the carrier of [:t,f:] -defined the carrier of S -valued Function-like V26( the carrier of [:t,f:]) quasi_total Element of bool [: the carrier of [:t,f:], the carrier of S:]

f +* P is Relation-like Function-like set

c

x2 is closed Element of bool the carrier of T

dom f is non empty Element of bool the carrier of [:s,f:]

the carrier of f is non empty set

[: the carrier of t, the carrier of f:] is non empty Relation-like set

dom (f +* P) is set

dom P is non empty Element of bool the carrier of [:t,f:]

(dom f) \/ (dom P) is non empty set

rng (f +* P) is set

rng f is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

rng P is non empty Element of bool the carrier of S

(rng f) \/ (rng P) is non empty Element of bool the carrier of S

[: the carrier of s, the carrier of f:] is non empty Relation-like set

[: the carrier of T, the carrier of f:] is non empty Relation-like set

ls2 is non empty Relation-like the carrier of [:T,f:] -defined the carrier of S -valued Function-like V26( the carrier of [:T,f:]) quasi_total Element of bool [: the carrier of [:T,f:], the carrier of S:]

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

[#] f is non empty non proper open closed Element of bool the carrier of f

bool the carrier of f is non empty set

[:c

a2 is Element of bool the carrier of S

ls2 " a2 is Element of bool the carrier of [:T,f:]

P2 is set

(ls2 " a2) /\ ([#] [:t,f:]) is Element of bool the carrier of [:t,f:]

P " a2 is Element of bool the carrier of [:t,f:]

ls2 . P2 is set

P . P2 is set

P . P2 is set

ls2 . P2 is set

dom ls2 is non empty Element of bool the carrier of [:T,f:]

P2 is set

ls2 . P2 is set

f . P2 is set

P . P2 is set

P2 is set

(ls2 " a2) /\ ([#] [:s,f:]) is Element of bool the carrier of [:s,f:]

f " a2 is Element of bool the carrier of [:s,f:]

ls2 . P2 is set

f . P2 is set

f . P2 is set

ls2 . P2 is set

[#] [:T,f:] is non empty non proper open closed Element of bool the carrier of [:T,f:]

([#] [:s,f:]) \/ ([#] [:t,f:]) is non empty set

(ls2 " a2) /\ (([#] [:s,f:]) \/ ([#] [:t,f:])) is Element of bool the carrier of [:T,f:]

((ls2 " a2) /\ ([#] [:s,f:])) \/ ((ls2 " a2) /\ ([#] [:t,f:])) is set

(f " a2) \/ (P " a2) is set

a1 is Element of bool the carrier of [: