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
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a & not a + b <= b1 ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & not a + b <= b1 ) } is set
a + 0 is V28() real ext-real Element of REAL
].a,(a + b).] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a & b1 <= a + b ) } is set
a + 0 is V28() real ext-real Element of REAL
[.a,(a + b).] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= a + b ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a - b & not a <= b1 ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a - b <= b1 & not a <= b1 ) } is set
a - 0 is V28() real ext-real Element of REAL
].(a - b),a.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a - b & b1 <= a ) } is set
a - 0 is V28() real ext-real Element of REAL
[.(a - b),a.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( a - b <= b1 & b1 <= a ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a & not b <= b1 ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & not b <= b1 ) } is set
].a,b.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a & b1 <= b ) } is set
[.a,b.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= b ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a & not b <= b1 ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & not b <= b1 ) } is set
].a,b.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a & b1 <= b ) } is set
[.a,b.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= b ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a - s & not a + s <= b1 ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a - s & not a + s <= b1 ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( b <= b1 & b1 <= r ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= s ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= b & not r <= b1 ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= s ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= r & b1 <= b ) } is set
[.a,b.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= b ) } is set
b + 1 is V28() real ext-real Element of REAL
].r,(b + 1).[ is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= r & not b + 1 <= b1 ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & not r <= b1 ) } is set
[.a,b.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= b ) } is set
a - 1 is V28() real ext-real Element of REAL
].(a - 1),r.[ is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( not b1 <= a - 1 & not r <= b1 ) } is set
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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= 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
[:(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
{ b1 where b1 is V28() real ext-real Element of REAL : ( r <= b1 & b1 <= s ) } is set
[:[.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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= b ) } is 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)
[.r,s.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( r <= b1 & b1 <= s ) } 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
{ b1 where b1 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) : ( a <= b1 `1 & b1 `1 <= b & r <= b1 `2 & b1 `2 <= s ) } is set
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)
{ b1 where b1 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) : ( a <= b1 `1 & b1 `1 <= b & r <= b1 `2 & b1 `2 <= s ) } is set
|[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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= b ) } is set
[.r,s.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( r <= b1 & b1 <= s ) } is set
[:[.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
{ b1 where b1 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) : ( a <= b1 `1 & b1 `1 <= b & r <= b1 `2 & b1 `2 <= s ) } is set
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):]
{ b1 where b1 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) : ( a <= b1 `1 & b1 `1 <= b & r <= b1 `2 & b1 `2 <= s ) } is 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)
|[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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= b ) } is set
[.r,s.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( r <= b1 & b1 <= s ) } is set
[:[.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
{ b1 where b1 is V28() real ext-real Element of REAL : ( a <= b1 & b1 <= b ) } is set
[.r,s.] is V176() V177() V178() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : ( r <= b1 & b1 <= s ) } is set
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,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 closed V176() V177() V178() Element of bool the carrier of (Closed-Interval-TSpace (a,b))
B is closed 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)