:: TOPREALA semantic presentation

REAL is non empty V30() V176() V177() V178() V182() set

NAT is V176() V177() V178() V179() V180() V181() V182() Element of bool REAL

bool REAL is set

omega is V176() V177() V178() V179() V180() V181() V182() set

bool omega is set

bool NAT is set

[:REAL,REAL:] is Relation-like V166() V167() V168() set

bool [:REAL,REAL:] is set

COMPLEX is non empty V30() V176() V182() set

RAT is non empty V30() V176() V177() V178() V179() V182() set

INT is non empty V30() V176() V177() V178() V179() V180() V182() set

K374() is non empty V125() L9()

the carrier of K374() is non empty set

<REAL,+> is non empty V125() V147() V148() V149() V151() left-invertible right-invertible V200() left-cancelable right-cancelable V203() L9()

K380() is non empty V125() V149() V151() left-cancelable right-cancelable V203() SubStr of <REAL,+>

<NAT,+> is non empty V125() V147() V149() V151() left-cancelable right-cancelable V203() uniquely-decomposable SubStr of K380()

<REAL,*> is non empty V125() V147() V149() V151() L9()

<NAT,*> is non empty V125() V147() V149() V151() uniquely-decomposable SubStr of <REAL,*>

1 is non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() Element of NAT

[:1,1:] is Relation-like RAT -valued INT -valued V166() V167() V168() V169() set

bool [:1,1:] is set

[:[:1,1:],1:] is Relation-like RAT -valued INT -valued V166() V167() V168() V169() set

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

[:[:1,1:],REAL:] is Relation-like V166() V167() V168() set

bool [:[:1,1:],REAL:] is set

[:[:REAL,REAL:],REAL:] is Relation-like V166() V167() V168() set

bool [:[:REAL,REAL:],REAL:] is set

2 is non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() Element of NAT

[:2,2:] is Relation-like RAT -valued INT -valued V166() V167() V168() V169() set

[:[:2,2:],REAL:] is Relation-like V166() V167() V168() set

bool [:[:2,2:],REAL:] is set

K478() is non empty strict TopSpace-like V227() TopStruct

the carrier of K478() is non empty V176() V177() V178() set

K420() is V208() V227() L14()

R^1 is non empty strict TopSpace-like V227() TopStruct

K485() is non empty strict TopSpace-like V227() SubSpace of R^1

TOP-REAL 2 is non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() L16()

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

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

{} is set

the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V30() FinSequence-like FinSubsequence-like FinSequence-membered V166() V167() V168() V169() V176() V177() V178() V179() V180() V181() V182() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V30() FinSequence-like FinSubsequence-like FinSequence-membered V166() V167() V168() V169() V176() V177() V178() V179() V180() V181() V182() set

3 is non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() Element of NAT

the carrier of R^1 is non empty V176() V177() V178() set

0 is natural V28() real ext-real integer V110() V176() V177() V178() V179() V180() V181() Element of NAT

[:R^1,R^1:] is non empty strict TopSpace-like TopStruct

the carrier of [:R^1,R^1:] is non empty set

[: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):] is Relation-like set

bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):] is set

bool {} is set

{{}} is set

Seg 1 is non empty V30() V37(1) V176() V177() V178() V179() V180() V181() Element of bool NAT

{1} is V176() V177() V178() V179() V180() V181() set

Seg 2 is non empty V30() V37(2) V176() V177() V178() V179() V180() V181() Element of bool NAT

{1,2} is V176() V177() V178() V179() V180() V181() set

bool the carrier of R^1 is set

[: the carrier of R^1, the carrier of R^1:] is Relation-like V166() V167() V168() set

a is V28() real ext-real set

b is non empty V28() real ext-real positive non negative set

a + b is V28() real ext-real set

].a,(a + b).[ is V176() V177() V178() Element of bool REAL

{ b

a + 0 is V28() real ext-real Element of REAL

a + (a + b) is V28() real ext-real set

(a + (a + b)) / 2 is V28() real ext-real Element of REAL

[.a,(a + b).[ is V176() V177() V178() Element of bool REAL

{ b

a + 0 is V28() real ext-real Element of REAL

].a,(a + b).] is V176() V177() V178() Element of bool REAL

{ b

a + 0 is V28() real ext-real Element of REAL

[.a,(a + b).] is V176() V177() V178() Element of bool REAL

{ b

a + 0 is V28() real ext-real Element of REAL

a - b is V28() real ext-real set

].(a - b),a.[ is V176() V177() V178() Element of bool REAL

{ b

a - 0 is V28() real ext-real Element of REAL

(a - b) + a is V28() real ext-real set

((a - b) + a) / 2 is V28() real ext-real Element of REAL

[.(a - b),a.[ is V176() V177() V178() Element of bool REAL

{ b

a - 0 is V28() real ext-real Element of REAL

].(a - b),a.] is V176() V177() V178() Element of bool REAL

{ b

a - 0 is V28() real ext-real Element of REAL

[.(a - b),a.] is V176() V177() V178() Element of bool REAL

{ b

a - 0 is V28() real ext-real Element of REAL

a is V28() real ext-real non positive set

b is non empty V28() real ext-real positive non negative set

].a,b.[ is V176() V177() V178() Element of bool REAL

{ b

a + b is V28() real ext-real set

(a + b) / 2 is V28() real ext-real Element of REAL

[.a,b.[ is V176() V177() V178() Element of bool REAL

{ b

].a,b.] is V176() V177() V178() Element of bool REAL

{ b

[.a,b.] is V176() V177() V178() Element of bool REAL

{ b

a is non empty V28() real ext-real non positive negative set

b is V28() real ext-real non negative set

].a,b.[ is V176() V177() V178() Element of bool REAL

{ b

a + b is V28() real ext-real set

(a + b) / 2 is V28() real ext-real Element of REAL

[.a,b.[ is V176() V177() V178() Element of bool REAL

{ b

].a,b.] is V176() V177() V178() Element of bool REAL

{ b

[.a,b.] is V176() V177() V178() Element of bool REAL

{ b

a is Relation-like Function-like set

dom a is set

b is set

a . b is set

r is set

a .: r is set

s is set

a . s is set

a is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

dom a is V176() V177() V178() V179() V180() V181() Element of bool NAT

b is natural V28() real ext-real set

b + 1 is V28() real ext-real Element of REAL

1 + 0 is V28() real ext-real Element of REAL

len a is natural V28() real ext-real integer V110() V176() V177() V178() V179() V180() V181() Element of NAT

a is set

b is set

r is set

s is set

(a,b) --> (r,s) is Relation-like Function-like set

product ((a,b) --> (r,s)) is set

T is Relation-like Function-like set

T . a is set

T . b is set

dom ((a,b) --> (r,s)) is set

{a,b} is set

((a,b) --> (r,s)) . b is set

((a,b) --> (r,s)) . a is set

a is set

b is set

<*a,b*> is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like set

(1,2) --> (a,b) is Relation-like REAL -defined Function-like set

dom ((1,2) --> (a,b)) is V176() V177() V178() Element of bool REAL

T is set

((1,2) --> (a,b)) . T is set

<*a,b*> . T is set

((1,2) --> (a,b)) . T is set

<*a,b*> . T is set

dom <*a,b*> is non empty V176() V177() V178() V179() V180() V181() Element of bool NAT

Euclid 1 is non empty V208() V213() V214() V215() V216() L14()

REAL 1 is functional non empty FinSequence-membered M14( REAL )

K346(1,REAL) is functional FinSequence-membered M14( REAL )

Pitag_dist 1 is Relation-like [:(REAL 1),(REAL 1):] -defined REAL -valued Function-like total quasi_total V166() V167() V168() Element of bool [:[:(REAL 1),(REAL 1):],REAL:]

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

[:[:(REAL 1),(REAL 1):],REAL:] is Relation-like V166() V167() V168() set

bool [:[:(REAL 1),(REAL 1):],REAL:] is set

G14((REAL 1),(Pitag_dist 1)) is V208() L14()

TopSpaceMetr (Euclid 1) is non empty strict TopSpace-like TopStruct

a is non empty strict TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

TOP-REAL 1 is non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() L16()

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

the topology of (TOP-REAL 1) is non empty Element of bool (bool the carrier of (TOP-REAL 1))

bool the carrier of (TOP-REAL 1) is set

bool (bool the carrier of (TOP-REAL 1)) is set

TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is non empty strict TopSpace-like TopStruct

a is TopSpace-like constituted-Functions constituted-FinSeqs TopStruct

b is TopSpace-like SubSpace of a

the carrier of b is set

r is Element of the carrier of b

the carrier of a is set

bool the carrier of a is set

s is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of a

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is non empty TopSpace-like SubSpace of a

the carrier of b is non empty set

bool the carrier of b is set

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

r is Element of the carrier of a

s is Element of the carrier of b

T is non empty open a_neighborhood of r

T /\ ([#] b) is Element of bool the carrier of b

S is Element of bool the carrier of b

Int S is open Element of bool the carrier of b

Int T is open Element of bool the carrier of a

bool the carrier of a is set

a is TopSpace-like TopStruct

the carrier of a is set

bool the carrier of a is set

{{}, the carrier of a} is set

a is TopSpace-like discrete TopStruct

the carrier of a is set

b is TopSpace-like TopStruct

the carrier of b is set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is Relation-like the carrier of a -defined the carrier of b -valued Function-like quasi_total Element of bool [: the carrier of a, the carrier of b:]

a is TopSpace-like TopStruct

the carrier of a is set

b is TopStruct

the carrier of b is set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is Relation-like the carrier of a -defined the carrier of b -valued Function-like quasi_total Element of bool [: the carrier of a, the carrier of b:]

bool the carrier of b is set

s is Element of bool the carrier of b

r " s is Element of bool the carrier of a

bool the carrier of a is set

{} a is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V30() FinSequence-like FinSubsequence-like FinSequence-membered open closed boundary nowhere_dense V166() V167() V168() V169() V176() V177() V178() V179() V180() V181() V182() Element of bool the carrier of a

a is TopSpace-like TopStruct

the carrier of a is set

b is TopStruct

the carrier of b is set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is Relation-like the carrier of a -defined the carrier of b -valued Function-like quasi_total Element of bool [: the carrier of a, the carrier of b:]

a is TopStruct

the carrier of a is set

b is non empty TopStruct

the carrier of b is non empty set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is non empty SubSpace of b

the carrier of r is non empty set

[: the carrier of a, the carrier of r:] is Relation-like set

bool [: the carrier of a, the carrier of r:] is set

s is Relation-like the carrier of a -defined the carrier of r -valued Function-like total quasi_total Element of bool [: the carrier of a, the carrier of r:]

bool the carrier of b is set

rng s is Element of bool the carrier of r

bool the carrier of r is set

dom s is Element of bool the carrier of a

bool the carrier of a is set

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

bool the carrier of a is set

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

bool the carrier of b is set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is Element of bool the carrier of a

a | r is strict TopSpace-like SubSpace of a

the carrier of (a | r) is set

s is Element of bool the carrier of b

b | s is strict TopSpace-like SubSpace of b

the carrier of (b | s) is set

[: the carrier of (a | r), the carrier of (b | s):] is Relation-like set

bool [: the carrier of (a | r), the carrier of (b | s):] is set

T is Relation-like the carrier of a -defined the carrier of b -valued Function-like non empty total quasi_total continuous Element of bool [: the carrier of a, the carrier of b:]

T | r is Relation-like the carrier of a -defined r -defined the carrier of a -defined the carrier of b -valued Function-like Element of bool [: the carrier of a, the carrier of b:]

S is Relation-like the carrier of (a | r) -defined the carrier of (b | s) -valued Function-like quasi_total Element of bool [: the carrier of (a | r), the carrier of (b | s):]

rng (T | r) is Element of bool the carrier of b

dom T is non empty Element of bool the carrier of a

dom (T | r) is Element of bool r

bool r is set

[: the carrier of (a | r), the carrier of b:] is Relation-like set

bool [: the carrier of (a | r), the carrier of b:] is set

A is Relation-like the carrier of (a | r) -defined the carrier of b -valued Function-like total quasi_total Element of bool [: the carrier of (a | r), the carrier of b:]

b is non empty TopSpace-like TopStruct

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

the carrier of b is non empty set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is non empty TopSpace-like SubSpace of b

the carrier of r is non empty set

[: the carrier of a, the carrier of r:] is Relation-like set

bool [: the carrier of a, the carrier of r:] is set

s is Relation-like the carrier of a -defined the carrier of b -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of b:]

T is Relation-like the carrier of a -defined the carrier of r -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of r:]

S is Element of the carrier of a

T . S is Element of the carrier of r

h is non empty open a_neighborhood of S

T .: h is Element of bool the carrier of r

bool the carrier of r is set

s . S is Element of the carrier of b

s .: h is Element of bool the carrier of b

bool the carrier of b is set

A is non empty open a_neighborhood of s . S

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

A /\ ([#] r) is Element of bool the carrier of r

B is Element of bool the carrier of r

P is non empty a_neighborhood of T . S

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

bool the carrier of a is set

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

bool the carrier of b is set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is Element of bool the carrier of a

a | r is strict TopSpace-like SubSpace of a

the carrier of (a | r) is set

s is Element of bool the carrier of b

b | s is strict TopSpace-like SubSpace of b

the carrier of (b | s) is set

[: the carrier of (a | r), the carrier of (b | s):] is Relation-like set

bool [: the carrier of (a | r), the carrier of (b | s):] is set

T is Relation-like the carrier of a -defined the carrier of b -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of b:]

T | r is Relation-like the carrier of a -defined r -defined the carrier of a -defined the carrier of b -valued Function-like Element of bool [: the carrier of a, the carrier of b:]

S is Relation-like the carrier of (a | r) -defined the carrier of (b | s) -valued Function-like quasi_total Element of bool [: the carrier of (a | r), the carrier of (b | s):]

rng S is Element of bool the carrier of (b | s)

bool the carrier of (b | s) is set

bool the carrier of (a | r) is set

h is Element of bool the carrier of (a | r)

S .: h is Element of bool the carrier of (b | s)

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

[#] (a | r) is non proper open closed dense Element of bool the carrier of (a | r)

A is Element of bool the carrier of a

A /\ ([#] (a | r)) is Element of bool the carrier of (a | r)

A /\ r is Element of bool the carrier of a

S .: (A /\ r) is Element of bool the carrier of (b | s)

S .: A is Element of bool the carrier of (b | s)

S .: r is Element of bool the carrier of (b | s)

(S .: A) /\ (S .: r) is Element of bool the carrier of (b | s)

T .: A is Element of bool the carrier of b

(T .: A) /\ s is Element of bool the carrier of b

B is set

dom S is Element of bool the carrier of (a | r)

dom T is non empty Element of bool the carrier of a

P is Element of the carrier of a

T . P is Element of the carrier of b

S0 is set

S . S0 is set

T . S0 is set

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

[: the carrier of b, the carrier of r:] is Relation-like set

bool [: the carrier of b, the carrier of r:] is set

s is Relation-like the carrier of a -defined the carrier of b -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of b:]

T is Relation-like the carrier of b -defined the carrier of r -valued Function-like non empty total quasi_total Element of bool [: the carrier of b, the carrier of r:]

T * s is Relation-like the carrier of a -defined the carrier of r -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of r:]

[: the carrier of a, the carrier of r:] is Relation-like set

bool [: the carrier of a, the carrier of r:] is set

bool the carrier of a is set

S is Element of bool the carrier of a

(T * s) .: S is Element of bool the carrier of r

bool the carrier of r is set

s .: S is Element of bool the carrier of b

bool the carrier of b is set

T .: (s .: S) is Element of bool the carrier of r

b is TopSpace-like TopStruct

a is TopSpace-like TopStruct

the carrier of a is set

the carrier of b is set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is TopSpace-like open SubSpace of b

the carrier of r is set

[: the carrier of a, the carrier of r:] is Relation-like set

bool [: the carrier of a, the carrier of r:] is set

s is Relation-like the carrier of a -defined the carrier of b -valued Function-like quasi_total Element of bool [: the carrier of a, the carrier of b:]

T is Relation-like the carrier of a -defined the carrier of r -valued Function-like quasi_total Element of bool [: the carrier of a, the carrier of r:]

bool the carrier of a is set

S is Element of bool the carrier of a

s .: S is Element of bool the carrier of b

bool the carrier of b is set

T .: S is Element of bool the carrier of r

bool the carrier of r is set

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is Relation-like the carrier of a -defined the carrier of b -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of b:]

r " is Relation-like the carrier of b -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of b, the carrier of a:]

[: the carrier of b, the carrier of a:] is Relation-like set

bool [: the carrier of b, the carrier of a:] is set

r " is Relation-like Function-like set

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

bool the carrier of b is set

s is Element of bool the carrier of b

(r ") .: s is Element of bool the carrier of a

bool the carrier of a is set

r " s is Element of bool the carrier of a

s is Element of bool the carrier of b

(r ") .: s is Element of bool the carrier of a

bool the carrier of a is set

r " s is Element of bool the carrier of a

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is Relation-like the carrier of a -defined the carrier of b -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of b:]

r " is Relation-like the carrier of b -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of b, the carrier of a:]

[: the carrier of b, the carrier of a:] is Relation-like set

bool [: the carrier of b, the carrier of a:] is set

rng r is non empty Element of bool the carrier of b

bool the carrier of b is set

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

rng (r ") is non empty Element of bool the carrier of a

bool the carrier of a is set

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

(r ") " is Relation-like the carrier of a -defined the carrier of b -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of b:]

a is TopSpace-like TopStruct

the carrier of a is set

the topology of a is non empty Element of bool (bool the carrier of a)

bool the carrier of a is set

bool (bool the carrier of a) is set

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

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

the topology of b is non empty Element of bool (bool the carrier of b)

bool the carrier of b is set

bool (bool the carrier of b) is set

TopStruct(# the carrier of b, the topology of b #) is non empty strict TopSpace-like TopStruct

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

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

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

bool the carrier of TopStruct(# the carrier of a, the topology of a #) is set

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

[#] TopStruct(# the carrier of b, the topology of b #) is non empty non proper open closed dense non boundary Element of bool the carrier of TopStruct(# the carrier of b, the topology of b #)

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

bool the carrier of TopStruct(# the carrier of b, the topology of b #) is set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

T is Relation-like the carrier of a -defined the carrier of b -valued Function-like total quasi_total Element of bool [: the carrier of a, the carrier of b:]

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

bool [: the carrier of TopStruct(# the carrier of a, the topology of a #), the carrier of TopStruct(# the carrier of b, the topology of b #):] is set

h is Element of bool the carrier of TopStruct(# the carrier of a, the topology of a #)

S is Relation-like the carrier of TopStruct(# the carrier of a, the topology of a #) -defined the carrier of TopStruct(# the carrier of b, the topology of b #) -valued Function-like total quasi_total Element of bool [: the carrier of TopStruct(# the carrier of a, the topology of a #), the carrier of TopStruct(# the carrier of b, the topology of b #):]

Cl h is closed Element of bool the carrier of TopStruct(# the carrier of a, the topology of a #)

S .: (Cl h) is Element of bool the carrier of TopStruct(# the carrier of b, the topology of b #)

A is Element of bool the carrier of a

Cl A is closed Element of bool the carrier of a

T .: (Cl A) is Element of bool the carrier of b

T .: A is Element of bool the carrier of b

Cl (T .: A) is closed Element of bool the carrier of b

S .: h is Element of bool the carrier of TopStruct(# the carrier of b, the topology of b #)

Cl (S .: h) is closed Element of bool the carrier of TopStruct(# the carrier of b, the topology of b #)

dom T is Element of bool the carrier of a

rng T is Element of bool the carrier of b

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

bool [: the carrier of TopStruct(# the carrier of a, the topology of a #), the carrier of TopStruct(# the carrier of b, the topology of b #):] is set

T is Relation-like the carrier of TopStruct(# the carrier of a, the topology of a #) -defined the carrier of TopStruct(# the carrier of b, the topology of b #) -valued Function-like total quasi_total Element of bool [: the carrier of TopStruct(# the carrier of a, the topology of a #), the carrier of TopStruct(# the carrier of b, the topology of b #):]

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

h is Element of bool the carrier of a

S is Relation-like the carrier of a -defined the carrier of b -valued Function-like total quasi_total Element of bool [: the carrier of a, the carrier of b:]

Cl h is closed Element of bool the carrier of a

S .: (Cl h) is Element of bool the carrier of b

A is Element of bool the carrier of TopStruct(# the carrier of a, the topology of a #)

Cl A is closed Element of bool the carrier of TopStruct(# the carrier of a, the topology of a #)

T .: (Cl A) is Element of bool the carrier of TopStruct(# the carrier of b, the topology of b #)

T .: A is Element of bool the carrier of TopStruct(# the carrier of b, the topology of b #)

Cl (T .: A) is closed Element of bool the carrier of TopStruct(# the carrier of b, the topology of b #)

S .: h is Element of bool the carrier of b

Cl (S .: h) is closed Element of bool the carrier of b

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

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

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

[: the carrier of a, the carrier of b:] is Relation-like set

bool [: the carrier of a, the carrier of b:] is set

r is Relation-like the carrier of a -defined the carrier of b -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of b:]

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

bool the carrier of b is set

dom r is non empty Element of bool the carrier of a

bool the carrier of a is set

s is Element of bool the carrier of a

r .: s is Element of bool the carrier of b

r " (r .: s) is Element of bool the carrier of a

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

rng r is non empty Element of bool the carrier of b

a is V28() real ext-real set

REAL --> a is Relation-like REAL -defined {a} -valued Function-like quasi_total V166() V167() V168() Element of bool [:REAL,{a}:]

{a} is V176() V177() V178() set

[:REAL,{a}:] is Relation-like V166() V167() V168() set

bool [:REAL,{a}:] is set

b is Relation-like REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

b | REAL is Relation-like REAL -defined REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

r is V28() real ext-real Element of REAL

dom (b | REAL) is V176() V177() V178() Element of bool REAL

s is V28() real ext-real Element of REAL

(b | REAL) . s is V28() real ext-real set

b . s is V28() real ext-real set

a is Relation-like REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

dom a is V176() V177() V178() Element of bool REAL

b is Relation-like REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

dom b is V176() V177() V178() Element of bool REAL

r is Relation-like REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

dom r is V176() V177() V178() Element of bool REAL

(dom b) \/ (dom r) is V176() V177() V178() Element of bool REAL

b | (dom b) is Relation-like REAL -defined dom b -defined REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

r | (dom r) is Relation-like REAL -defined dom r -defined REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

a | (dom a) is Relation-like REAL -defined dom a -defined REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

(dom a) /\ (dom b) is V176() V177() V178() Element of bool REAL

a | (dom r) is Relation-like REAL -defined dom r -defined REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

dom (a | (dom r)) is V176() V177() V178() Element of bool REAL

(dom a) /\ (dom r) is V176() V177() V178() Element of bool REAL

S is V28() real ext-real set

dom (a | (dom a)) is V176() V177() V178() Element of bool REAL

a | ((dom b) \/ (dom r)) is Relation-like REAL -defined (dom b) \/ (dom r) -defined REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

(a | ((dom b) \/ (dom r))) . S is V28() real ext-real set

a . S is V28() real ext-real set

a | (dom b) is Relation-like REAL -defined dom b -defined REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

dom (a | (dom b)) is V176() V177() V178() Element of bool REAL

b . S is V28() real ext-real set

(b | (dom b)) . S is V28() real ext-real set

dom (a | ((dom b) \/ (dom r))) is V176() V177() V178() Element of bool ((dom b) \/ (dom r))

bool ((dom b) \/ (dom r)) is set

h is V176() V177() V178() Neighbourhood of (a | ((dom b) \/ (dom r))) . S

A is V176() V177() V178() Neighbourhood of S

dom (b | (dom b)) is V176() V177() V178() Element of bool REAL

B is V176() V177() V178() Neighbourhood of S

P is V176() V177() V178() Neighbourhood of S

S0 is V28() real ext-real set

(a | ((dom b) \/ (dom r))) . S0 is V28() real ext-real set

(dom b) /\ (dom b) is V176() V177() V178() Element of bool REAL

a . S0 is V28() real ext-real set

b . S0 is V28() real ext-real set

(b | (dom b)) . S0 is V28() real ext-real set

r . S is V28() real ext-real set

(r | (dom r)) . S is V28() real ext-real set

dom (a | ((dom b) \/ (dom r))) is V176() V177() V178() Element of bool ((dom b) \/ (dom r))

bool ((dom b) \/ (dom r)) is set

h is V176() V177() V178() Neighbourhood of (a | ((dom b) \/ (dom r))) . S

A is V176() V177() V178() Neighbourhood of S

dom (r | (dom r)) is V176() V177() V178() Element of bool REAL

B is V176() V177() V178() Neighbourhood of S

P is V176() V177() V178() Neighbourhood of S

S0 is V28() real ext-real set

(a | ((dom b) \/ (dom r))) . S0 is V28() real ext-real set

(dom r) /\ (dom r) is V176() V177() V178() Element of bool REAL

a . S0 is V28() real ext-real set

r . S0 is V28() real ext-real set

(r | (dom r)) . S0 is V28() real ext-real set

a is V28() real ext-real Element of the carrier of R^1

b is V176() V177() V178() Element of bool REAL

r is V176() V177() V178() Element of bool the carrier of R^1

s is V28() real ext-real set

a - s is V28() real ext-real set

a + s is V28() real ext-real set

].(a - s),(a + s).[ is V176() V177() V178() Element of bool REAL

{ b

a is V28() real ext-real Element of the carrier of R^1

b is non empty V176() V177() V178() a_neighborhood of a

r is V176() V177() V178() Element of bool the carrier of R^1

s is V28() real ext-real Element of REAL

a - s is V28() real ext-real Element of REAL

a + s is V28() real ext-real Element of REAL

].(a - s),(a + s).[ is V176() V177() V178() Element of bool REAL

{ b

T is V176() V177() V178() Neighbourhood of a

bool [: the carrier of R^1, the carrier of R^1:] is set

a is Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like non empty total quasi_total V166() V167() V168() Element of bool [: the carrier of R^1, the carrier of R^1:]

b is Relation-like REAL -defined REAL -valued Function-like V166() V167() V168() Element of bool [:REAL,REAL:]

r is V28() real ext-real Element of the carrier of R^1

a . r is V28() real ext-real Element of the carrier of R^1

s is non empty V176() V177() V178() a_neighborhood of a . r

b . r is V28() real ext-real set

T is V176() V177() V178() Neighbourhood of b . r

S is V176() V177() V178() Neighbourhood of r

b .: S is V176() V177() V178() Element of bool REAL

h is non empty V176() V177() V178() a_neighborhood of r

a .: h is V176() V177() V178() Element of bool the carrier of R^1

a is Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like non empty total quasi_total V166() V167() V168() Element of bool [: the carrier of R^1, the carrier of R^1:]

b is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total V166() V167() V168() Element of bool [:REAL,REAL:]

r is V28() real ext-real Element of the carrier of R^1

dom a is non empty V176() V177() V178() Element of bool the carrier of R^1

dom b is non empty V176() V177() V178() Element of bool REAL

a is V28() real ext-real set

b is V28() real ext-real set

r is V28() real ext-real set

[.b,r.] is V176() V177() V178() Element of bool REAL

{ b

s is V28() real ext-real set

Closed-Interval-TSpace (a,s) is non empty strict TopSpace-like V227() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (a,s)) is non empty V176() V177() V178() set

bool the carrier of (Closed-Interval-TSpace (a,s)) is set

{} (Closed-Interval-TSpace (a,s)) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V30() FinSequence-like FinSubsequence-like FinSequence-membered open closed boundary nowhere_dense V166() V167() V168() V169() V176() V177() V178() V179() V180() V181() V182() Element of bool the carrier of (Closed-Interval-TSpace (a,s))

[.a,s.] is V176() V177() V178() Element of bool REAL

{ b

h is V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,s))

A is V176() V177() V178() Element of bool the carrier of R^1

[#] (Closed-Interval-TSpace (a,s)) is non empty non proper open closed dense non boundary V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,s))

A /\ ([#] (Closed-Interval-TSpace (a,s))) is V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,s))

a is V28() real ext-real set

b is V28() real ext-real set

r is V28() real ext-real set

].b,r.[ is V176() V177() V178() Element of bool REAL

{ b

s is V28() real ext-real set

Closed-Interval-TSpace (a,s) is non empty strict TopSpace-like V227() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (a,s)) is non empty V176() V177() V178() set

bool the carrier of (Closed-Interval-TSpace (a,s)) is set

{} (Closed-Interval-TSpace (a,s)) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V30() FinSequence-like FinSubsequence-like FinSequence-membered open closed boundary nowhere_dense V166() V167() V168() V169() V176() V177() V178() V179() V180() V181() V182() Element of bool the carrier of (Closed-Interval-TSpace (a,s))

[.a,s.] is V176() V177() V178() Element of bool REAL

{ b

h is V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,s))

A is V176() V177() V178() Element of bool the carrier of R^1

[#] (Closed-Interval-TSpace (a,s)) is non empty non proper open closed dense non boundary V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,s))

A /\ ([#] (Closed-Interval-TSpace (a,s))) is V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,s))

a is V28() real ext-real set

b is V28() real ext-real set

Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V227() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (a,b)) is non empty V176() V177() V178() set

bool the carrier of (Closed-Interval-TSpace (a,b)) is set

r is V28() real ext-real set

].r,b.] is V176() V177() V178() Element of bool REAL

{ b

[.a,b.] is V176() V177() V178() Element of bool REAL

{ b

b + 1 is V28() real ext-real Element of REAL

].r,(b + 1).[ is V176() V177() V178() Element of bool REAL

{ b

S is V176() V177() V178() Element of bool the carrier of R^1

[#] (Closed-Interval-TSpace (a,b)) is non empty non proper open closed dense non boundary V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,b))

S /\ ([#] (Closed-Interval-TSpace (a,b))) is V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,b))

T is V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,b))

h is set

A is V28() real ext-real Element of REAL

b + 0 is V28() real ext-real Element of REAL

a is V28() real ext-real set

b is V28() real ext-real set

Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V227() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (a,b)) is non empty V176() V177() V178() set

bool the carrier of (Closed-Interval-TSpace (a,b)) is set

r is V28() real ext-real set

[.a,r.[ is V176() V177() V178() Element of bool REAL

{ b

[.a,b.] is V176() V177() V178() Element of bool REAL

{ b

a - 1 is V28() real ext-real Element of REAL

].(a - 1),r.[ is V176() V177() V178() Element of bool REAL

{ b

S is V176() V177() V178() Element of bool the carrier of R^1

[#] (Closed-Interval-TSpace (a,b)) is non empty non proper open closed dense non boundary V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,b))

S /\ ([#] (Closed-Interval-TSpace (a,b))) is V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,b))

T is V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,b))

h is set

A is V28() real ext-real Element of REAL

a - 0 is V28() real ext-real Element of REAL

a is V28() real ext-real set

b is V28() real ext-real set

Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V227() SubSpace of R^1

[.a,b.] is V176() V177() V178() Element of bool REAL

{ b

r is V28() real ext-real set

s is V28() real ext-real set

Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like V227() SubSpace of R^1

[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is non empty strict TopSpace-like TopStruct

the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is non empty set

[.r,s.] is V176() V177() V178() Element of bool REAL

{ b

[:[.a,b.],[.r,s.]:] is Relation-like V166() V167() V168() set

the carrier of (Closed-Interval-TSpace (a,b)) is non empty V176() V177() V178() set

the carrier of (Closed-Interval-TSpace (r,s)) is non empty V176() V177() V178() set

a is V28() real ext-real set

b is V28() real ext-real set

|[a,b]| is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

(1,2) --> (a,b) is Relation-like REAL -defined Function-like set

a is V28() real ext-real set

b is V28() real ext-real set

|[a,b]| is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

|[a,b]| . 1 is V28() real ext-real set

|[a,b]| . 2 is V28() real ext-real set

(1,2) --> (a,b) is Relation-like REAL -defined Function-like set

((1,2) --> (a,b)) . 1 is set

((1,2) --> (a,b)) . 2 is set

a is V28() real ext-real set

b is V28() real ext-real set

[.a,b.] is V176() V177() V178() Element of bool REAL

{ b

r is V28() real ext-real set

s is V28() real ext-real set

closed_inside_of_rectangle (a,b,r,s) is Element of bool the carrier of (TOP-REAL 2)

[.r,s.] is V176() V177() V178() Element of bool REAL

{ b

(1,2) --> ([.a,b.],[.r,s.]) is Relation-like REAL -defined Function-like set

product ((1,2) --> ([.a,b.],[.r,s.])) is set

{ b

B is set

P is Relation-like NAT -defined Function-like V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

P `1 is V28() real ext-real Element of REAL

K526(P,1) is V28() real ext-real Element of REAL

P `2 is V28() real ext-real Element of REAL

K526(P,2) is V28() real ext-real Element of REAL

|[(P `1),(P `2)]| is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

(1,2) --> ((P `1),(P `2)) is Relation-like REAL -defined {1,2} -defined REAL -valued Function-like total quasi_total V166() V167() V168() Element of bool [:{1,2},REAL:]

[:{1,2},REAL:] is Relation-like V166() V167() V168() set

bool [:{1,2},REAL:] is set

B is set

dom ((1,2) --> ([.a,b.],[.r,s.])) is V176() V177() V178() Element of bool REAL

P is Relation-like Function-like set

dom P is set

P . 2 is set

P . 1 is set

y is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

len y is natural V28() real ext-real integer V110() V176() V177() V178() V179() V180() V181() Element of NAT

S0 is V28() real ext-real Element of REAL

g is V28() real ext-real Element of REAL

|[S0,g]| is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

(1,2) --> (S0,g) is Relation-like REAL -defined {1,2} -defined REAL -valued Function-like total quasi_total V166() V167() V168() Element of bool [:{1,2},REAL:]

[:{1,2},REAL:] is Relation-like V166() V167() V168() set

bool [:{1,2},REAL:] is set

p is Relation-like NAT -defined Function-like V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

p `2 is V28() real ext-real Element of REAL

K526(p,2) is V28() real ext-real Element of REAL

p `1 is V28() real ext-real Element of REAL

K526(p,1) is V28() real ext-real Element of REAL

a is V28() real ext-real set

b is V28() real ext-real set

r is V28() real ext-real set

|[a,r]| is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

s is V28() real ext-real set

closed_inside_of_rectangle (a,b,r,s) is Element of bool the carrier of (TOP-REAL 2)

{ b

|[a,r]| `1 is V28() real ext-real Element of REAL

K526(|[a,r]|,1) is V28() real ext-real Element of REAL

|[a,r]| `2 is V28() real ext-real Element of REAL

K526(|[a,r]|,2) is V28() real ext-real Element of REAL

a is V28() real ext-real set

b is V28() real ext-real set

r is V28() real ext-real set

s is V28() real ext-real set

closed_inside_of_rectangle (a,b,r,s) is Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,r,s)) is strict TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

a is V28() real ext-real set

b is V28() real ext-real set

r is V28() real ext-real set

s is V28() real ext-real set

(a,b,r,s) is TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

closed_inside_of_rectangle (a,b,r,s) is Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,r,s)) is strict TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

|[a,r]| is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

the carrier of (a,b,r,s) is set

a is V28() real ext-real non positive set

r is V28() real ext-real non negative set

b is V28() real ext-real non positive set

s is V28() real ext-real non negative set

(a,r,b,s) is TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

closed_inside_of_rectangle (a,r,b,s) is Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (closed_inside_of_rectangle (a,r,b,s)) is strict TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

a is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

a is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

b is V28() real ext-real set

r is V28() real ext-real set

[b,r] is set

{b,r} is V176() V177() V178() set

{b} is V176() V177() V178() set

{{b,r},{b}} is set

a . [b,r] is set

<*b,r*> is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like set

a is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

b is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

r is Element of the carrier of [:R^1,R^1:]

a . r is set

b . r is set

s is V28() real ext-real Element of the carrier of R^1

T is V28() real ext-real Element of the carrier of R^1

[s,T] is Element of the carrier of [:R^1,R^1:]

{s,T} is V176() V177() V178() set

{s} is V176() V177() V178() set

{{s,T},{s}} is set

a . r is Relation-like NAT -defined Function-like V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

<*s,T*> is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like set

b . r is Relation-like NAT -defined Function-like V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

() is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

a is V28() real ext-real Element of REAL

b is V28() real ext-real Element of REAL

[a,b] is set

{a,b} is V176() V177() V178() set

{a} is V176() V177() V178() set

{{a,b},{a}} is set

() . [a,b] is set

<*a,b*> is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like set

a is V176() V177() V178() Element of bool REAL

b is V176() V177() V178() Element of bool REAL

[:a,b:] is Relation-like V166() V167() V168() set

() .: [:a,b:] is Element of bool the carrier of (TOP-REAL 2)

(1,2) --> (a,b) is Relation-like REAL -defined Function-like set

product ((1,2) --> (a,b)) is set

a is V28() real ext-real Element of REAL

b is V28() real ext-real Element of REAL

[a,b] is set

{a,b} is V176() V177() V178() set

{a} is V176() V177() V178() set

{{a,b},{a}} is set

() . [a,b] is set

<*a,b*> is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like set

a is V28() real ext-real set

b is V28() real ext-real set

Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V227() SubSpace of R^1

r is V28() real ext-real set

s is V28() real ext-real set

Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like V227() SubSpace of R^1

[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is non empty strict TopSpace-like TopStruct

the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is non empty set

() | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] -defined the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

(a,b,r,s) is TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

closed_inside_of_rectangle (a,b,r,s) is Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,r,s)) is strict TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

the carrier of (a,b,r,s) is set

[: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):] is Relation-like set

bool [: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):] is set

[.a,b.] is V176() V177() V178() Element of bool REAL

{ b

[.r,s.] is V176() V177() V178() Element of bool REAL

{ b

[:[.a,b.],[.r,s.]:] is Relation-like V166() V167() V168() set

dom () is non empty Element of bool the carrier of [:R^1,R^1:]

bool the carrier of [:R^1,R^1:] is set

dom (() | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) is Element of bool the carrier of [:R^1,R^1:]

rng (() | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) is Element of bool the carrier of (TOP-REAL 2)

B is set

{ b

P is set

(() | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . P is set

S0 is Element of the carrier of [:R^1,R^1:]

g is V28() real ext-real Element of the carrier of R^1

y is V28() real ext-real Element of the carrier of R^1

[g,y] is Element of the carrier of [:R^1,R^1:]

{g,y} is V176() V177() V178() set

{g} is V176() V177() V178() set

{{g,y},{g}} is set

(() | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . S0 is set

() . S0 is Relation-like NAT -defined Function-like V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

<*g,y*> is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like set

p is Relation-like NAT -defined Function-like V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

p `2 is V28() real ext-real Element of REAL

K526(p,2) is V28() real ext-real Element of REAL

p `1 is V28() real ext-real Element of REAL

K526(p,1) is V28() real ext-real Element of REAL

a is V28() real ext-real set

b is V28() real ext-real set

Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V227() SubSpace of R^1

r is V28() real ext-real set

s is V28() real ext-real set

Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like V227() SubSpace of R^1

[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is non empty strict TopSpace-like TopStruct

the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is non empty set

(a,b,r,s) is TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

closed_inside_of_rectangle (a,b,r,s) is Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,r,s)) is strict TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

the carrier of (a,b,r,s) is set

[: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):] is Relation-like set

bool [: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):] is set

() | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] -defined the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

{ b

|[a,r]| is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

|[a,r]| `1 is V28() real ext-real Element of REAL

K526(|[a,r]|,1) is V28() real ext-real Element of REAL

|[a,r]| `2 is V28() real ext-real Element of REAL

K526(|[a,r]|,2) is V28() real ext-real Element of REAL

P is Relation-like the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] -defined the carrier of (a,b,r,s) -valued Function-like quasi_total Element of bool [: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):]

S0 is non empty TopSpace-like SubSpace of [:R^1,R^1:]

the carrier of S0 is non empty set

h is non empty TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

the carrier of h is non empty set

[: the carrier of S0, the carrier of h:] is Relation-like set

bool [: the carrier of S0, the carrier of h:] is set

g is Relation-like the carrier of S0 -defined the carrier of h -valued Function-like non empty total quasi_total Element of bool [: the carrier of S0, the carrier of h:]

rng g is non empty Element of bool the carrier of h

bool the carrier of h is set

y is set

[.a,b.] is V176() V177() V178() Element of bool REAL

{ b

[.r,s.] is V176() V177() V178() Element of bool REAL

{ b

[:[.a,b.],[.r,s.]:] is Relation-like V166() V167() V168() set

dom g is non empty Element of bool the carrier of S0

bool the carrier of S0 is set

p is Relation-like NAT -defined Function-like V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

p `1 is V28() real ext-real Element of REAL

K526(p,1) is V28() real ext-real Element of REAL

p `2 is V28() real ext-real Element of REAL

K526(p,2) is V28() real ext-real Element of REAL

[(p `1),(p `2)] is set

{(p `1),(p `2)} is V176() V177() V178() set

{(p `1)} is V176() V177() V178() set

{{(p `1),(p `2)},{(p `1)}} is set

g . [(p `1),(p `2)] is set

() . [(p `1),(p `2)] is set

|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V30() V37(2) FinSequence-like FinSubsequence-like V166() V167() V168() Element of the carrier of (TOP-REAL 2)

() | S0 is Relation-like the carrier of S0 -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of S0, the carrier of (TOP-REAL 2):]

[: the carrier of S0, the carrier of (TOP-REAL 2):] is Relation-like set

bool [: the carrier of S0, the carrier of (TOP-REAL 2):] is set

() | the carrier of S0 is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of S0 -defined the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

a is V28() real ext-real set

b is V28() real ext-real set

Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V227() SubSpace of R^1

r is V28() real ext-real set

s is V28() real ext-real set

Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like V227() SubSpace of R^1

[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is non empty strict TopSpace-like TopStruct

(a,b,r,s) is TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

closed_inside_of_rectangle (a,b,r,s) is Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,r,s)) is strict TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is non empty set

the carrier of (a,b,r,s) is set

[: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):] is Relation-like set

bool [: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):] is set

() | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] -defined the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

h is Relation-like the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] -defined the carrier of (a,b,r,s) -valued Function-like quasi_total Element of bool [: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):]

a is V28() real ext-real set

b is V28() real ext-real set

Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V227() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (a,b)) is non empty V176() V177() V178() set

bool the carrier of (Closed-Interval-TSpace (a,b)) is set

r is V28() real ext-real set

s is V28() real ext-real set

Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like V227() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (r,s)) is non empty V176() V177() V178() set

bool the carrier of (Closed-Interval-TSpace (r,s)) is set

(a,b,r,s) is TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

closed_inside_of_rectangle (a,b,r,s) is Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,r,s)) is strict TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

the carrier of (a,b,r,s) is set

bool the carrier of (a,b,r,s) is set

[.a,b.] is V176() V177() V178() Element of bool REAL

{ b

[.r,s.] is V176() V177() V178() Element of bool REAL

{ b

h is V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,b))

A is V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (r,s))

(1,2) --> (h,A) is Relation-like REAL -defined Function-like set

product ((1,2) --> (h,A)) is set

(1,2) --> ([.a,b.],[.r,s.]) is Relation-like REAL -defined Function-like set

product ((1,2) --> ([.a,b.],[.r,s.])) is set

a is V28() real ext-real set

b is V28() real ext-real set

Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V227() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (a,b)) is non empty V176() V177() V178() set

bool the carrier of (Closed-Interval-TSpace (a,b)) is set

r is V28() real ext-real set

s is V28() real ext-real set

Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like V227() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (r,s)) is non empty V176() V177() V178() set

bool the carrier of (Closed-Interval-TSpace (r,s)) is set

(a,b,r,s) is TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

closed_inside_of_rectangle (a,b,r,s) is Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,r,s)) is strict TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

the carrier of (a,b,r,s) is set

bool the carrier of (a,b,r,s) is set

[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is non empty strict TopSpace-like TopStruct

the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is non empty set

[: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):] is Relation-like set

bool [: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):] is set

() | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] -defined the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

A is open V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,b))

B is open V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (r,s))

(1,2) --> (A,B) is Relation-like REAL -defined Function-like set

product ((1,2) --> (A,B)) is set

[:A,B:] is Relation-like V166() V167() V168() Element of bool the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]

bool the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is set

h is Relation-like the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] -defined the carrier of (a,b,r,s) -valued Function-like quasi_total Element of bool [: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], the carrier of (a,b,r,s):]

h .: [:A,B:] is Element of bool the carrier of (a,b,r,s)

() .: [:A,B:] is Element of bool the carrier of (TOP-REAL 2)

P is Element of bool the carrier of (a,b,r,s)

a is V28() real ext-real set

b is V28() real ext-real set

Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V227() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (a,b)) is non empty V176() V177() V178() set

bool the carrier of (Closed-Interval-TSpace (a,b)) is set

r is V28() real ext-real set

s is V28() real ext-real set

Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like V227() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (r,s)) is non empty V176() V177() V178() set

bool the carrier of (Closed-Interval-TSpace (r,s)) is set

(a,b,r,s) is TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

closed_inside_of_rectangle (a,b,r,s) is Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,r,s)) is strict TopSpace-like constituted-Functions constituted-FinSeqs SubSpace of TOP-REAL 2

the carrier of (a,b,r,s) is set

bool the carrier of (a,b,r,