REAL is non empty V32() complex-membered ext-real-membered real-membered V209() set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool REAL
bool REAL is non empty set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 V74() compact real-membered pathwise_connected SubSpace of R^1
R^1 is non empty strict TopSpace-like real-membered TopStruct
the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set
omega is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() set
bool omega is non empty set
bool NAT is non empty set
{} is empty trivial Relation-like non-empty empty-yielding complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() set
the empty trivial Relation-like non-empty empty-yielding complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() set is empty trivial Relation-like non-empty empty-yielding complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() set
1 is non empty natural V11() real ext-real positive non negative V172() V173() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
{{},1} is non empty set
COMPLEX is non empty V32() complex-membered V209() set
RAT is non empty V32() complex-membered ext-real-membered real-membered rational-membered V209() set
INT is non empty V32() complex-membered ext-real-membered real-membered rational-membered integer-membered V209() set
[:REAL,REAL:] is non empty Relation-like set
bool [:REAL,REAL:] is non empty set
K457() is non empty V100() L9()
the carrier of K457() is non empty set
K462() is non empty V100() V174() V175() V176() V178() V225() V226() V227() V228() V229() V230() L9()
K463() is non empty V100() V176() V178() V228() V229() V230() M32(K462())
K464() is non empty V100() V174() V176() V178() V228() V229() V230() V231() M35(K462(),K463())
K466() is non empty V100() V174() V176() V178() L9()
K467() is non empty V100() V174() V176() V178() V231() M32(K466())
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 V74() compact real-membered pathwise_connected TopStruct
the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set
[:1,1:] is non empty Relation-like set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty Relation-like set
bool [:[:1,1:],REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty Relation-like set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty natural V11() real ext-real positive non negative V172() V173() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
[:2,2:] is non empty Relation-like set
[:[:2,2:],REAL:] is non empty Relation-like set
bool [:[:2,2:],REAL:] is non empty set
K551() is V237() real-membered L18()
0 is empty trivial natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding V172() V173() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of NAT
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (0,1)) is non empty complex-membered ext-real-membered real-membered set
TOP-REAL 2 is non empty TopSpace-like V98() V123() V124() V125() V126() V127() V128() V129() V215() V216() V257() L19()
the carrier of (TOP-REAL 2) is non empty set
NonZero (TOP-REAL 2) is Element of bool the carrier of (TOP-REAL 2)
bool the carrier of (TOP-REAL 2) is non empty set
[#] (TOP-REAL 2) is non empty non proper open closed Element of bool the carrier of (TOP-REAL 2)
K164((TOP-REAL 2)) is Relation-like Function-like V39(2) FinSequence-like V55( TOP-REAL 2) V195() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
{K164((TOP-REAL 2))} is non empty trivial set
([#] (TOP-REAL 2)) \ {K164((TOP-REAL 2))} is Element of bool the carrier of (TOP-REAL 2)
[:(NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)):] is Relation-like set
bool [:(NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)):] is non empty set
[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is non empty Relation-like set
bool [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is non empty set
K638(K551()) is TopStruct
the carrier of K638(K551()) is set
bool the carrier of K638(K551()) is non empty set
[.0,1.] is complex-membered ext-real-membered real-membered Element of bool REAL
0[01] is V11() real ext-real Element of the carrier of I[01]
1[01] is V11() real ext-real Element of the carrier of I[01]
(#) (0,1) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(0,1) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set
bool the carrier of I[01] is non empty set
1 / 2 is V11() real ext-real non negative Element of REAL
[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 compact TopStruct
the carrier of [:I[01],I[01]:] is non empty set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : b1 `2 <= b1 `1 } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : b1 `1 <= b1 `2 } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : - (b1 `1) <= b1 `2 } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : b1 `2 <= - (b1 `1) } is set
[: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 non empty Relation-like set
bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):] is non empty set
1 / 2 is V11() real ext-real non negative set
F1() is non empty set
T is set
T is set
T is Relation-like Function-like set
proj1 T is set
T is Relation-like Function-like set
proj1 T is set
a is Element of F1()
T . a is set
F2(a) is set
F3(a) is set
F4(a) is set
[:[.0,1.],[.0,1.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]
T is V11() real ext-real set
b is V11() real ext-real set
a is V11() real ext-real set
b - T is V11() real ext-real set
a - T is V11() real ext-real set
(b - T) / (a - T) is V11() real ext-real set
T is V11() real ext-real Element of the carrier of I[01]
2 * T is V11() real ext-real Element of REAL
2 * (1 / 2) is V11() real ext-real non negative Element of REAL
T is V11() real ext-real Element of the carrier of I[01]
2 * T is V11() real ext-real Element of REAL
(2 * T) - 1 is V11() real ext-real Element of REAL
2 * 1 is V11() real ext-real non negative Element of REAL
2 - 1 is V11() real ext-real Element of REAL
2 * (1 / 2) is V11() real ext-real non negative Element of REAL
1 - 1 is V11() real ext-real Element of REAL
T is V11() real ext-real Element of the carrier of I[01]
a is V11() real ext-real Element of the carrier of I[01]
T * a is V11() real ext-real set
T is V11() real ext-real Element of the carrier of I[01]
(1 / 2) * T is V11() real ext-real Element of REAL
(1 / 2) * 1 is V11() real ext-real non negative Element of REAL
4 is non empty natural V11() real ext-real positive non negative V172() V173() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 / 4 is V11() real ext-real non negative Element of REAL
T is V11() real ext-real Element of the carrier of I[01]
T - (1 / 4) is V11() real ext-real Element of REAL
1 + (1 / 4) is non empty V11() real ext-real positive non negative Element of REAL
(1 / 4) + 0 is V11() real ext-real non negative Element of REAL
id I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V43( the carrier of I[01]) quasi_total continuous being_homeomorphism V171( I[01] , I[01] ) Element of bool [: the carrier of I[01], the carrier of I[01]:]
[: the carrier of I[01], the carrier of I[01]:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of I[01]:] is non empty set
id the carrier of I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued V43( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of I[01]:]
(id I[01]) . 0 is set
(id I[01]) . 1 is set
bool the carrier of [:I[01],I[01]:] is non empty set
T is V11() real ext-real Element of the carrier of I[01]
a is V11() real ext-real Element of the carrier of I[01]
b is V11() real ext-real Element of the carrier of I[01]
P is V11() real ext-real Element of the carrier of I[01]
[.T,a.] is complex-membered ext-real-membered real-membered Element of bool REAL
[.b,P.] is complex-membered ext-real-membered real-membered Element of bool REAL
[:[.T,a.],[.b,P.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]
Q is non empty Element of bool the carrier of [:I[01],I[01]:]
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : b1 `2 <= (2 * (b1 `1)) - 1 } is set
AffineMap (1,0,(1 / 2),(1 / 2)) is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of (TOP-REAL 2)) quasi_total continuous Element of bool [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):]
Q is Element of bool the carrier of (TOP-REAL 2)
e2 is Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(1 / 2))) .: Q is Element of bool the carrier of (TOP-REAL 2)
gg is set
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)
gg is set
(AffineMap (1,0,(1 / 2),(1 / 2))) . gg is set
S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S2 `2 is V11() real ext-real Element of REAL
K599(S2,2) is V11() real ext-real Element of REAL
S2 `1 is V11() real ext-real Element of REAL
K599(S2,1) is V11() real ext-real Element of REAL
2 * (S2 `1) is V11() real ext-real Element of REAL
(2 * (S2 `1)) - 1 is V11() real ext-real Element of REAL
(AffineMap (1,0,(1 / 2),(1 / 2))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
1 * (S2 `1) is V11() real ext-real Element of REAL
(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL
(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL
((1 / 2) * (S2 `2)) + (1 / 2) is V11() real ext-real Element of REAL
|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (1 / 2))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `1 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),1) is V11() real ext-real Element of REAL
((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),2) is V11() real ext-real Element of REAL
(1 / 2) * ((2 * (S2 `1)) - 1) is V11() real ext-real Element of REAL
(S2 `1) - (1 / 2) is V11() real ext-real Element of REAL
((S2 `1) - (1 / 2)) + (1 / 2) is V11() real ext-real Element of REAL
gg is set
rng (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)
gg is set
(AffineMap (1,0,(1 / 2),(1 / 2))) . gg is set
S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(1 / 2))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S2 `1 is V11() real ext-real Element of REAL
K599(S2,1) is V11() real ext-real Element of REAL
1 * (S2 `1) is V11() real ext-real Element of REAL
(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL
S2 `2 is V11() real ext-real Element of REAL
K599(S2,2) is V11() real ext-real Element of REAL
(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL
((1 / 2) * (S2 `2)) + (1 / 2) is V11() real ext-real Element of REAL
|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (1 / 2))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `1 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),1) is V11() real ext-real Element of REAL
((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),2) is V11() real ext-real Element of REAL
2 * (((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2) is V11() real ext-real Element of REAL
2 * (S2 `1) is V11() real ext-real Element of REAL
g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
g `2 is V11() real ext-real Element of REAL
K599(g,2) is V11() real ext-real Element of REAL
g `1 is V11() real ext-real Element of REAL
K599(g,1) is V11() real ext-real Element of REAL
(2 * (((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2)) - 1 is V11() real ext-real Element of REAL
(2 * (S2 `1)) - 1 is V11() real ext-real Element of REAL
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : (2 * (b1 `1)) - 1 <= b1 `2 } is set
Q is Element of bool the carrier of (TOP-REAL 2)
e2 is Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(1 / 2))) .: Q is Element of bool the carrier of (TOP-REAL 2)
gg is set
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)
gg is set
(AffineMap (1,0,(1 / 2),(1 / 2))) . gg is set
S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S2 `1 is V11() real ext-real Element of REAL
K599(S2,1) is V11() real ext-real Element of REAL
2 * (S2 `1) is V11() real ext-real Element of REAL
(2 * (S2 `1)) - 1 is V11() real ext-real Element of REAL
S2 `2 is V11() real ext-real Element of REAL
K599(S2,2) is V11() real ext-real Element of REAL
(1 / 2) * ((2 * (S2 `1)) - 1) is V11() real ext-real Element of REAL
(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL
(AffineMap (1,0,(1 / 2),(1 / 2))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
1 * (S2 `1) is V11() real ext-real Element of REAL
(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL
((1 / 2) * (S2 `2)) + (1 / 2) is V11() real ext-real Element of REAL
|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (1 / 2))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `1 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),1) is V11() real ext-real Element of REAL
((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),2) is V11() real ext-real Element of REAL
(S2 `1) - (1 / 2) is V11() real ext-real Element of REAL
((S2 `1) - (1 / 2)) + (1 / 2) is V11() real ext-real Element of REAL
gg is set
rng (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)
gg is set
(AffineMap (1,0,(1 / 2),(1 / 2))) . gg is set
S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(1 / 2))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S2 `1 is V11() real ext-real Element of REAL
K599(S2,1) is V11() real ext-real Element of REAL
1 * (S2 `1) is V11() real ext-real Element of REAL
(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL
S2 `2 is V11() real ext-real Element of REAL
K599(S2,2) is V11() real ext-real Element of REAL
(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL
((1 / 2) * (S2 `2)) + (1 / 2) is V11() real ext-real Element of REAL
|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (1 / 2))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `1 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),1) is V11() real ext-real Element of REAL
2 * (S2 `1) is V11() real ext-real Element of REAL
((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),2) is V11() real ext-real Element of REAL
2 * (((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2) is V11() real ext-real Element of REAL
g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
g `1 is V11() real ext-real Element of REAL
K599(g,1) is V11() real ext-real Element of REAL
g `2 is V11() real ext-real Element of REAL
K599(g,2) is V11() real ext-real Element of REAL
(2 * (S2 `1)) - 1 is V11() real ext-real Element of REAL
(2 * (((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2)) - 1 is V11() real ext-real Element of REAL
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : 1 - (2 * (b1 `1)) <= b1 `2 } is set
- (1 / 2) is V11() real ext-real non positive Element of REAL
AffineMap (1,0,(1 / 2),(- (1 / 2))) is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of (TOP-REAL 2)) quasi_total continuous Element of bool [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):]
Q is Element of bool the carrier of (TOP-REAL 2)
e2 is Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: Q is Element of bool the carrier of (TOP-REAL 2)
gg is set
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)
gg is set
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . gg is set
S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S2 `1 is V11() real ext-real Element of REAL
K599(S2,1) is V11() real ext-real Element of REAL
2 * (S2 `1) is V11() real ext-real Element of REAL
1 - (2 * (S2 `1)) is V11() real ext-real Element of REAL
S2 `2 is V11() real ext-real Element of REAL
K599(S2,2) is V11() real ext-real Element of REAL
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (1 - (2 * (S2 `1))) is V11() real ext-real Element of REAL
(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL
(1 / 2) - (S2 `1) is V11() real ext-real Element of REAL
((1 / 2) - (S2 `1)) + (- (1 / 2)) is V11() real ext-real Element of REAL
((1 / 2) * (S2 `2)) + (- (1 / 2)) is V11() real ext-real Element of REAL
1 * (S2 `1) is V11() real ext-real Element of REAL
(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL
|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (- (1 / 2)))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),1) is V11() real ext-real Element of REAL
- (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1) is V11() real ext-real Element of REAL
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),2) is V11() real ext-real Element of REAL
gg is set
rng (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)
gg is set
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . gg is set
S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S2 `1 is V11() real ext-real Element of REAL
K599(S2,1) is V11() real ext-real Element of REAL
1 * (S2 `1) is V11() real ext-real Element of REAL
(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL
S2 `2 is V11() real ext-real Element of REAL
K599(S2,2) is V11() real ext-real Element of REAL
(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL
((1 / 2) * (S2 `2)) + (- (1 / 2)) is V11() real ext-real Element of REAL
|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (- (1 / 2)))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),1) is V11() real ext-real Element of REAL
- (S2 `1) is V11() real ext-real Element of REAL
2 * (- (S2 `1)) is V11() real ext-real Element of REAL
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),2) is V11() real ext-real Element of REAL
2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2) is V11() real ext-real Element of REAL
g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
g `1 is V11() real ext-real Element of REAL
K599(g,1) is V11() real ext-real Element of REAL
- (g `1) is V11() real ext-real Element of REAL
g `2 is V11() real ext-real Element of REAL
K599(g,2) is V11() real ext-real Element of REAL
(2 * (- (S2 `1))) + 1 is V11() real ext-real Element of REAL
(2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2)) + 1 is V11() real ext-real Element of REAL
2 * (S2 `1) is V11() real ext-real Element of REAL
1 - (2 * (S2 `1)) is V11() real ext-real Element of REAL
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : b1 `2 <= 1 - (2 * (b1 `1)) } is set
Q is Element of bool the carrier of (TOP-REAL 2)
e2 is Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: Q is Element of bool the carrier of (TOP-REAL 2)
gg is set
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)
gg is set
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . gg is set
S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S2 `2 is V11() real ext-real Element of REAL
K599(S2,2) is V11() real ext-real Element of REAL
S2 `1 is V11() real ext-real Element of REAL
K599(S2,1) is V11() real ext-real Element of REAL
2 * (S2 `1) is V11() real ext-real Element of REAL
1 - (2 * (S2 `1)) is V11() real ext-real Element of REAL
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL
(1 / 2) * (1 - (2 * (S2 `1))) is V11() real ext-real Element of REAL
((1 / 2) * (S2 `2)) + (- (1 / 2)) is V11() real ext-real Element of REAL
(1 / 2) - (S2 `1) is V11() real ext-real Element of REAL
((1 / 2) - (S2 `1)) + (- (1 / 2)) is V11() real ext-real Element of REAL
1 * (S2 `1) is V11() real ext-real Element of REAL
(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL
|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (- (1 / 2)))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),1) is V11() real ext-real Element of REAL
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),2) is V11() real ext-real Element of REAL
- (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1) is V11() real ext-real Element of REAL
gg is set
rng (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)
gg is set
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . gg is set
S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S2 `1 is V11() real ext-real Element of REAL
K599(S2,1) is V11() real ext-real Element of REAL
1 * (S2 `1) is V11() real ext-real Element of REAL
(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL
S2 `2 is V11() real ext-real Element of REAL
K599(S2,2) is V11() real ext-real Element of REAL
(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL
((1 / 2) * (S2 `2)) + (- (1 / 2)) is V11() real ext-real Element of REAL
|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (- (1 / 2)))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),1) is V11() real ext-real Element of REAL
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2 is V11() real ext-real Element of REAL
K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),2) is V11() real ext-real Element of REAL
2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2) is V11() real ext-real Element of REAL
- (S2 `1) is V11() real ext-real Element of REAL
2 * (- (S2 `1)) is V11() real ext-real Element of REAL
g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
g `2 is V11() real ext-real Element of REAL
K599(g,2) is V11() real ext-real Element of REAL
g `1 is V11() real ext-real Element of REAL
K599(g,1) is V11() real ext-real Element of REAL
- (g `1) is V11() real ext-real Element of REAL
(2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2)) + 1 is V11() real ext-real Element of REAL
(2 * (- (S2 `1))) + 1 is V11() real ext-real Element of REAL
2 * (S2 `1) is V11() real ext-real Element of REAL
1 - (2 * (S2 `1)) is V11() real ext-real Element of REAL
T is non empty 1-sorted
the carrier of T is non empty set
a is Element of the carrier of T
a is set
T is real-membered 1-sorted
the carrier of T is complex-membered ext-real-membered real-membered set
a is V11() real ext-real Element of the carrier of T
T is real-membered TopStruct
a is real-membered SubSpace of T
T is non empty TopSpace-like real-membered TopStruct
a is non empty TopSpace-like real-membered TopStruct
[:T,a:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,a:] is non empty set
b is Element of the carrier of [:T,a:]
b `1 is set
the carrier of T is non empty complex-membered ext-real-membered real-membered set
the carrier of a is non empty complex-membered ext-real-membered real-membered set
[: the carrier of T, the carrier of a:] is non empty Relation-like set
b `2 is set
the carrier of T is non empty complex-membered ext-real-membered real-membered set
the carrier of a is non empty complex-membered ext-real-membered real-membered set
[: the carrier of T, the carrier of a:] is non empty Relation-like set
T is non empty TopSpace-like T_0 T_1 T_2 SubSpace of [:I[01],I[01]:]
the carrier of T is non empty set
a is Element of the carrier of T
a `1 is set
b is Element of the carrier of [:I[01],I[01]:]
b `1 is V11() real ext-real set
a `2 is set
b is Element of the carrier of [:I[01],I[01]:]
b `2 is V11() real ext-real set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
b is Element of bool the carrier of (TOP-REAL 2)
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(1 / 2))) .: b is Element of bool the carrier of (TOP-REAL 2)
T is closed Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(1 / 2))) " ((AffineMap (1,0,(1 / 2),(1 / 2))) .: b) is Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
b is Element of bool the carrier of (TOP-REAL 2)
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(1 / 2))) .: b is Element of bool the carrier of (TOP-REAL 2)
T is closed Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(1 / 2))) " ((AffineMap (1,0,(1 / 2),(1 / 2))) .: b) is Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
b is Element of bool the carrier of (TOP-REAL 2)
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b is Element of bool the carrier of (TOP-REAL 2)
T is closed Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) " ((AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b) is Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
b is Element of bool the carrier of (TOP-REAL 2)
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b is Element of bool the carrier of (TOP-REAL 2)
T is closed Element of bool the carrier of (TOP-REAL 2)
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) " ((AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b) is Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : ( 1 - (2 * (b1 `1)) <= b1 `2 & (2 * (b1 `1)) - 1 <= b1 `2 ) } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : ( S2[b1] & S1[b1] ) } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S2[b1] } /\ { b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
a is closed Element of bool the carrier of (TOP-REAL 2)
T is closed Element of bool the carrier of (TOP-REAL 2)
a /\ T is closed Element of bool the carrier of (TOP-REAL 2)
REAL 2 is non empty FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
T is V11() real ext-real Element of REAL
a is V11() real ext-real Element of REAL
<*T,a*> is set
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is non empty set
[:[:REAL,REAL:],(REAL 2):] is non empty Relation-like set
bool [:[:REAL,REAL:],(REAL 2):] is non empty set
T is non empty Relation-like [:REAL,REAL:] -defined REAL 2 -valued Function-like V43([:REAL,REAL:]) quasi_total Element of bool [:[:REAL,REAL:],(REAL 2):]
[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set
a is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
b is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
[b,P] is non empty V29() set
{b,P} is non empty complex-membered ext-real-membered real-membered set
{b} is non empty trivial complex-membered ext-real-membered real-membered set
{{b,P},{b}} is non empty set
a . [b,P] is set
<*b,P*> is set
a . (b,P) is set
Q is Relation-like NAT -defined REAL -valued Function-like V39(2) FinSequence-like Element of REAL 2
b is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
[b,P] is non empty V29() set
{b,P} is non empty complex-membered ext-real-membered real-membered set
{b} is non empty trivial complex-membered ext-real-membered real-membered set
{{b,P},{b}} is non empty set
a . [b,P] is set
<*b,P*> is set
{ b1 where b1 is Element of the carrier of [:R^1,R^1:] : b1 `2 <= 1 - (2 * (b1 `1)) } is set
bool the carrier of [:R^1,R^1:] is non empty set
{ b1 where b1 is Element of the carrier of [:R^1,R^1:] : S1[b1] } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
P is Element of bool the carrier of (TOP-REAL 2)
b is Element of bool the carrier of [:R^1,R^1:]
Q .: b is Element of bool the carrier of (TOP-REAL 2)
Q is set
e2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
e2 `2 is V11() real ext-real Element of REAL
K599(e2,2) is V11() real ext-real Element of REAL
e2 `1 is V11() real ext-real Element of REAL
K599(e2,1) is V11() real ext-real Element of REAL
2 * (e2 `1) is V11() real ext-real Element of REAL
1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL
REAL 2 is non empty FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
gg is V11() real ext-real Element of REAL
gg is V11() real ext-real Element of REAL
<*gg,gg*> is set
2 * gg is V11() real ext-real Element of REAL
1 - (2 * gg) is V11() real ext-real Element of REAL
[gg,gg] is non empty V29() set
{gg,gg} is non empty complex-membered ext-real-membered real-membered set
{gg} is non empty trivial complex-membered ext-real-membered real-membered set
{{gg,gg},{gg}} is non empty set
g is Element of the carrier of [:R^1,R^1:]
dom Q is non empty Element of bool the carrier of [:R^1,R^1:]
g `1 is V11() real ext-real set
g `2 is V11() real ext-real set
Q . g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
Q is set
dom Q is non empty Element of bool the carrier of [:R^1,R^1:]
e2 is set
Q . e2 is set
gg is Element of the carrier of [:R^1,R^1:]
gg `2 is V11() real ext-real set
gg `1 is V11() real ext-real set
2 * (gg `1) is V11() real ext-real Element of REAL
1 - (2 * (gg `1)) is V11() real ext-real Element of REAL
[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set
gg is set
S2 is set
[gg,S2] is non empty V29() set
{gg,S2} is non empty set
{gg} is non empty trivial set
{{gg,S2},{gg}} is non empty set
g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
|[g,g]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S3 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S3 `1 is V11() real ext-real Element of REAL
K599(S3,1) is V11() real ext-real Element of REAL
S3 `2 is V11() real ext-real Element of REAL
K599(S3,2) is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of [:R^1,R^1:] : b1 `2 <= (2 * (b1 `1)) - 1 } is set
{ b1 where b1 is Element of the carrier of [:R^1,R^1:] : S1[b1] } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
P is Element of bool the carrier of (TOP-REAL 2)
b is Element of bool the carrier of [:R^1,R^1:]
Q .: b is Element of bool the carrier of (TOP-REAL 2)
Q is set
e2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
e2 `2 is V11() real ext-real Element of REAL
K599(e2,2) is V11() real ext-real Element of REAL
e2 `1 is V11() real ext-real Element of REAL
K599(e2,1) is V11() real ext-real Element of REAL
2 * (e2 `1) is V11() real ext-real Element of REAL
(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL
REAL 2 is non empty FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
gg is V11() real ext-real Element of REAL
gg is V11() real ext-real Element of REAL
<*gg,gg*> is set
2 * gg is V11() real ext-real Element of REAL
(2 * gg) - 1 is V11() real ext-real Element of REAL
[gg,gg] is non empty V29() set
{gg,gg} is non empty complex-membered ext-real-membered real-membered set
{gg} is non empty trivial complex-membered ext-real-membered real-membered set
{{gg,gg},{gg}} is non empty set
[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set
g is Element of the carrier of [:R^1,R^1:]
dom Q is non empty Element of bool the carrier of [:R^1,R^1:]
g `1 is V11() real ext-real set
g `2 is V11() real ext-real set
Q . g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
Q is set
dom Q is non empty Element of bool the carrier of [:R^1,R^1:]
e2 is set
Q . e2 is set
gg is Element of the carrier of [:R^1,R^1:]
gg `2 is V11() real ext-real set
gg `1 is V11() real ext-real set
2 * (gg `1) is V11() real ext-real Element of REAL
(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL
[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set
gg is set
S2 is set
[gg,S2] is non empty V29() set
{gg,S2} is non empty set
{gg} is non empty trivial set
{{gg,S2},{gg}} is non empty set
g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
|[g,g]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S3 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S3 `1 is V11() real ext-real Element of REAL
K599(S3,1) is V11() real ext-real Element of REAL
S3 `2 is V11() real ext-real Element of REAL
K599(S3,2) is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of [:R^1,R^1:] : ( 1 - (2 * (b1 `1)) <= b1 `2 & (2 * (b1 `1)) - 1 <= b1 `2 ) } is set
{ b1 where b1 is Element of the carrier of [:R^1,R^1:] : S1[b1] } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
P is Element of bool the carrier of (TOP-REAL 2)
b is Element of bool the carrier of [:R^1,R^1:]
Q .: b is Element of bool the carrier of (TOP-REAL 2)
Q is set
e2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
e2 `1 is V11() real ext-real Element of REAL
K599(e2,1) is V11() real ext-real Element of REAL
2 * (e2 `1) is V11() real ext-real Element of REAL
1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL
e2 `2 is V11() real ext-real Element of REAL
K599(e2,2) is V11() real ext-real Element of REAL
(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL
REAL 2 is non empty FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
gg is V11() real ext-real Element of REAL
gg is V11() real ext-real Element of REAL
<*gg,gg*> is set
2 * gg is V11() real ext-real Element of REAL
1 - (2 * gg) is V11() real ext-real Element of REAL
(2 * gg) - 1 is V11() real ext-real Element of REAL
[gg,gg] is non empty V29() set
{gg,gg} is non empty complex-membered ext-real-membered real-membered set
{gg} is non empty trivial complex-membered ext-real-membered real-membered set
{{gg,gg},{gg}} is non empty set
[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set
g is Element of the carrier of [:R^1,R^1:]
dom Q is non empty Element of bool the carrier of [:R^1,R^1:]
g `1 is V11() real ext-real set
g `2 is V11() real ext-real set
Q . g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
Q is set
dom Q is non empty Element of bool the carrier of [:R^1,R^1:]
e2 is set
Q . e2 is set
gg is Element of the carrier of [:R^1,R^1:]
gg `1 is V11() real ext-real set
2 * (gg `1) is V11() real ext-real Element of REAL
1 - (2 * (gg `1)) is V11() real ext-real Element of REAL
gg `2 is V11() real ext-real set
(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL
[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set
gg is set
S2 is set
[gg,S2] is non empty V29() set
{gg,S2} is non empty set
{gg} is non empty trivial set
{{gg,S2},{gg}} is non empty set
g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
|[g,g]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S3 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)
S3 `1 is V11() real ext-real Element of REAL
K599(S3,1) is V11() real ext-real Element of REAL
S3 `2 is V11() real ext-real Element of REAL
K599(S3,2) is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of [:I[01],I[01]:] : b1 `2 <= 1 - (2 * (b1 `1)) } is set
[0,0] is non empty V29() set
{0,0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{0} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{0,0},{0}} is non empty set
P is closed Element of bool the carrier of [:R^1,R^1:]
[#] [:I[01],I[01]:] is non empty non proper open closed Element of bool the carrier of [:I[01],I[01]:]
P /\ ([#] [:I[01],I[01]:]) is Element of bool the carrier of [:I[01],I[01]:]
Q is set
e2 is Element of the carrier of [:I[01],I[01]:]
e2 `2 is V11() real ext-real set
e2 `1 is V11() real ext-real set
2 * (e2 `1) is V11() real ext-real Element of REAL
1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL
e2 is Element of the carrier of [:R^1,R^1:]
e2 `2 is V11() real ext-real set
e2 `1 is V11() real ext-real set
2 * (e2 `1) is V11() real ext-real Element of REAL
1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL
gg is Element of the carrier of [:I[01],I[01]:]
gg `2 is V11() real ext-real set
gg `1 is V11() real ext-real set
2 * (gg `1) is V11() real ext-real Element of REAL
1 - (2 * (gg `1)) is V11() real ext-real Element of REAL
gg is Element of the carrier of [:I[01],I[01]:]
gg `2 is V11() real ext-real set
gg `1 is V11() real ext-real set
2 * (gg `1) is V11() real ext-real Element of REAL
1 - (2 * (gg `1)) is V11() real ext-real Element of REAL
Q is set
e2 is Element of the carrier of [:R^1,R^1:]
e2 `2 is V11() real ext-real set
e2 `1 is V11() real ext-real set
2 * (e2 `1) is V11() real ext-real Element of REAL
1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL
b is Element of the carrier of [:I[01],I[01]:]
b `1 is V11() real ext-real set
b `2 is V11() real ext-real set
2 * (b `1) is V11() real ext-real Element of REAL
1 - (2 * (b `1)) is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of [:I[01],I[01]:] : ( 1 - (2 * (b1 `1)) <= b1 `2 & (2 * (b1 `1)) - 1 <= b1 `2 ) } is set
[1,1] is non empty V29() set
{1,1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{1} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,1},{1}} is non empty set
b is Element of the carrier of [:I[01],I[01]:]
b `1 is V11() real ext-real set
2 * (b `1) is V11() real ext-real Element of REAL
(2 * (b `1)) - 1 is V11() real ext-real Element of REAL
b `2 is V11() real ext-real set
P is closed Element of bool the carrier of [:R^1,R^1:]
[#] [:I[01],I[01]:] is non empty non proper open closed Element of bool the carrier of [:I[01],I[01]:]
P /\ ([#] [:I[01],I[01]:]) is Element of bool the carrier of [:I[01],I[01]:]
Q is set
e2 is Element of the carrier of [:I[01],I[01]:]
e2 `1 is V11() real ext-real set
2 * (e2 `1) is V11() real ext-real Element of REAL
1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL
e2 `2 is V11() real ext-real set
(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL
e2 is Element of the carrier of [:R^1,R^1:]
e2 `1 is V11() real ext-real set
2 * (e2 `1) is V11() real ext-real Element of REAL
1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL
e2 `2 is V11() real ext-real set
gg is Element of the carrier of [:I[01],I[01]:]
gg `1 is V11() real ext-real set
2 * (gg `1) is V11() real ext-real Element of REAL
1 - (2 * (gg `1)) is V11() real ext-real Element of REAL
gg `2 is V11() real ext-real set
(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL
gg is Element of the carrier of [:I[01],I[01]:]
gg `1 is V11() real ext-real set
2 * (gg `1) is V11() real ext-real Element of REAL
1 - (2 * (gg `1)) is V11() real ext-real Element of REAL
gg `2 is V11() real ext-real set
(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL
gg is Element of the carrier of [:I[01],I[01]:]
gg `1 is V11() real ext-real set
2 * (gg `1) is V11() real ext-real Element of REAL
1 - (2 * (gg `1)) is V11() real ext-real Element of REAL
gg `2 is V11() real ext-real set
(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL
Q is set
e2 is Element of the carrier of [:R^1,R^1:]
e2 `1 is V11() real ext-real set
2 * (e2 `1) is V11() real ext-real Element of REAL
1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL
e2 `2 is V11() real ext-real set
(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL
1 - (2 * (b `1)) is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of [:I[01],I[01]:] : b1 `2 <= (2 * (b1 `1)) - 1 } is set
[1,0] is non empty V29() set
{1,0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{1} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,0},{1}} is non empty set
P is closed Element of bool the carrier of [:R^1,R^1:]
[#] [:I[01],I[01]:] is non empty non proper open closed Element of bool the carrier of [:I[01],I[01]:]
P /\ ([#] [:I[01],I[01]:]) is Element of bool the carrier of [:I[01],I[01]:]
Q is set
e2 is Element of the carrier of [:I[01],I[01]:]
e2 `2 is V11() real ext-real set
e2 `1 is V11() real ext-real set
2 * (e2 `1) is V11() real ext-real Element of REAL
(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL
e2 is Element of the carrier of [:R^1,R^1:]
e2 `2 is V11() real ext-real set
e2 `1 is V11() real ext-real set
2 * (e2 `1) is V11() real ext-real Element of REAL
(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL
gg is Element of the carrier of [:I[01],I[01]:]
gg `2 is V11() real ext-real set
gg `1 is V11() real ext-real set
2 * (gg `1) is V11() real ext-real Element of REAL
(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL
gg is Element of the carrier of [:I[01],I[01]:]
gg `2 is V11() real ext-real set
gg `1 is V11() real ext-real set
2 * (gg `1) is V11() real ext-real Element of REAL
(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL
Q is set
e2 is Element of the carrier of [:R^1,R^1:]
e2 `2 is V11() real ext-real set
e2 `1 is V11() real ext-real set
2 * (e2 `1) is V11() real ext-real Element of REAL
(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL
b is Element of the carrier of [:I[01],I[01]:]
b `1 is V11() real ext-real set
b `2 is V11() real ext-real set
2 * (b `1) is V11() real ext-real Element of REAL
(2 * (b `1)) - 1 is V11() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
a is non empty TopSpace-like TopStruct
[:T,a:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,a:] is non empty set
the carrier of T is non empty set
the carrier of a is non empty set
b is Element of the carrier of [:T,a:]
b `1 is set
b `2 is set
[: the carrier of T, the carrier of a:] is non empty Relation-like set
[.0,(1 / 2).] is complex-membered ext-real-membered real-membered Element of bool REAL
[:[.0,(1 / 2).],[.0,1.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]
[.(1 / 2),1.] is complex-membered ext-real-membered real-membered Element of bool REAL
[:[.(1 / 2),1.],[.0,1.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]
[#] [:I[01],I[01]:] is non empty non proper open closed Element of bool the carrier of [:I[01],I[01]:]
T is Element of bool the carrier of [:I[01],I[01]:]
a is Element of bool the carrier of [:I[01],I[01]:]
[:I[01],I[01]:] | T is strict TopSpace-like T_0 T_1 T_2 SubSpace of [:I[01],I[01]:]
[#] ([:I[01],I[01]:] | T) is non proper open closed Element of bool the carrier of ([:I[01],I[01]:] | T)
the carrier of ([:I[01],I[01]:] | T) is set
bool the carrier of ([:I[01],I[01]:] | T) is non empty set
[:I[01],I[01]:] | a is strict TopSpace-like T_0 T_1 T_2 SubSpace of [:I[01],I[01]:]
[#] ([:I[01],I[01]:] | a) is non proper open closed Element of bool the carrier of ([:I[01],I[01]:] | a)
the carrier of ([:I[01],I[01]:] | a) is set
bool the carrier of ([:I[01],I[01]:] | a) is non empty set
([#] ([:I[01],I[01]:] | T)) \/ ([#] ([:I[01],I[01]:] | a)) is set
T \/ ([#] ([:I[01],I[01]:] | a)) is set
T \/ a is Element of bool the carrier of [:I[01],I[01]:]
[.0,(1 / 2).] \/ [.(1 / 2),1.] is complex-membered ext-real-membered real-membered Element of bool REAL
[:([.0,(1 / 2).] \/ [.(1 / 2),1.]),[.0,1.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]
{(1 / 2)} is non empty trivial complex-membered ext-real-membered real-membered set
[:{(1 / 2)},[.0,1.]:] is Relation-like set
T is Element of bool the carrier of [:I[01],I[01]:]
a is Element of bool the carrier of [:I[01],I[01]:]
[:I[01],I[01]:] | a is strict TopSpace-like T_0 T_1 T_2 SubSpace of [:I[01],I[01]:]
the carrier of ([:I[01],I[01]:] | a) is set
[:I[01],I[01]:] | T is strict TopSpace-like T_0 T_1 T_2 SubSpace of [:I[01],I[01]:]
[#] ([:I[01],I[01]:] | T) is non proper open closed Element of bool the carrier of ([:I[01],I[01]:] | T)
the carrier of ([:I[01],I[01]:] | T) is set
bool the carrier of ([:I[01],I[01]:] | T) is non empty set
[#] ([:I[01],I[01]:] | a) is non proper open closed Element of bool the carrier of ([:I[01],I[01]:] | a)
bool the carrier of ([:I[01],I[01]:] | a) is non empty set
([#] ([:I[01],I[01]:] | T)) /\ ([#] ([:I[01],I[01]:] | a)) is Element of bool the carrier of ([:I[01],I[01]:] | a)
T /\ ([#] ([:I[01],I[01]:] | a)) is Element of bool the carrier of ([:I[01],I[01]:] | a)
T /\ a is Element of bool the carrier of [:I[01],I[01]:]
[.0,(1 / 2).] /\ [.(1 / 2),1.] is complex-membered ext-real-membered real-membered Element of bool REAL
[:([.0,(1 / 2).] /\ [.(1 / 2),1.]),[.0,1.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
{} T is empty trivial Relation-like non-empty empty-yielding compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of T
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
{} T is empty trivial Relation-like non-empty empty-yielding compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of T
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
a is V11() real ext-real set
b is V11() real ext-real set
[.a,b.] is complex-membered ext-real-membered real-membered Element of bool REAL
{} T is empty trivial Relation-like non-empty empty-yielding compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of T
T is V11() real ext-real Element of the carrier of I[01]
a is V11() real ext-real Element of the carrier of I[01]
[.T,a.] is complex-membered ext-real-membered real-membered Element of bool REAL
b is V11() real ext-real Element of the carrier of I[01]
P is V11() real ext-real Element of the carrier of I[01]
[.b,P.] is complex-membered ext-real-membered real-membered Element of bool REAL
[:[.T,a.],[.b,P.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]
Q is empty trivial proper Relation-like non-empty empty-yielding open closed compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of I[01]
[:Q,[.b,P.]:] is empty trivial proper Relation-like non-empty empty-yielding the carrier of I[01] -defined REAL -valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool [: the carrier of I[01],REAL:]
[: the carrier of I[01],REAL:] is non empty Relation-like set
bool [: the carrier of I[01],REAL:] is non empty set
Q is empty trivial proper Relation-like non-empty empty-yielding open closed compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of I[01]
[:[.T,a.],Q:] is empty trivial proper Relation-like non-empty empty-yielding REAL -defined the carrier of I[01] -valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool [:REAL, the carrier of I[01]:]
[:REAL, the carrier of I[01]:] is non empty Relation-like set
bool [:REAL, the carrier of I[01]:] is non empty set
Q is empty trivial proper Relation-like non-empty empty-yielding open closed compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of I[01]
[:[.T,a.],Q:] is empty trivial proper Relation-like non-empty empty-yielding REAL -defined the carrier of I[01] -valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool [:REAL, the carrier of I[01]:]
[:REAL, the carrier of I[01]:] is non empty Relation-like set
bool [:REAL, the carrier of I[01]:] is non empty set
T is V11() real ext-real set
a is V11() real ext-real set
Closed-Interval-TSpace (T,a) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,a)) is non empty complex-membered ext-real-membered real-membered set
b is V11() real ext-real set
P is V11() real ext-real set
Closed-Interval-TSpace (b,P) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (b,P)) is non empty complex-membered ext-real-membered real-membered set
P[01] (T,a,((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,a)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (T,a))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):]
[: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty set
(#) (b,P) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,P))
(b,P) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,P))
L[01] (((#) (b,P)),((b,P) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (b,P)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty set
(L[01] (((#) (b,P)),((b,P) (#)))) * (P[01] (T,a,((#) (0,1)),((0,1) (#)))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,a)) -defined the carrier of (Closed-Interval-TSpace (b,P)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (T,a))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):]
[: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty set
a is V11() real ext-real set
T is V11() real ext-real set
P is V11() real ext-real set
b is V11() real ext-real set
(T,a,b,P) is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,a)) -defined the carrier of (Closed-Interval-TSpace (b,P)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (T,a))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):]
Closed-Interval-TSpace (T,a) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,a)) is non empty complex-membered ext-real-membered real-membered set
Closed-Interval-TSpace (b,P) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (b,P)) is non empty complex-membered ext-real-membered real-membered set
[: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty set
P[01] (T,a,((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,a)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (T,a))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):]
[: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty set
(#) (b,P) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,P))
(b,P) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,P))
L[01] (((#) (b,P)),((b,P) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (b,P)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty set
(L[01] (((#) (b,P)),((b,P) (#)))) * (P[01] (T,a,((#) (0,1)),((0,1) (#)))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,a)) -defined the carrier of (Closed-Interval-TSpace (b,P)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (T,a))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):]
(T,a,b,P) . T is set
(T,a,b,P) . a is set
[.T,a.] is complex-membered ext-real-membered real-membered Element of bool REAL
dom (P[01] (T,a,((#) (0,1)),((0,1) (#)))) is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of (Closed-Interval-TSpace (T,a))
bool the carrier of (Closed-Interval-TSpace (T,a)) is non empty set
(P[01] (T,a,((#) (0,1)),((0,1) (#)))) . T is set
(L[01] (((#) (b,P)),((b,P) (#)))