:: BORSUK_6 semantic presentation

bool REAL is non empty set

bool omega is non empty set
bool NAT is non empty set

{{},1} is non empty set
COMPLEX is non empty V32() complex-membered V209() set

is non empty Relation-like set
bool 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())

[: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

bool is non empty set

[: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()

TOP-REAL 2 is non empty TopSpace-like V98() V123() V124() V125() V126() V127() V128() V129() V215() V216() V257() L19()
the carrier of () is non empty set
NonZero () is Element of bool the carrier of ()
bool the carrier of () is non empty set
[#] () is non empty non proper open closed Element of bool the carrier of ()
K164(()) is Relation-like Function-like V39(2) FinSequence-like V55( TOP-REAL 2) V195() Element of the carrier of ()
the ZeroF of () is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
{K164(())} is non empty trivial set
([#] ()) \ {K164(())} is Element of bool the carrier of ()
[:(NonZero ()),(NonZero ()):] is Relation-like set
bool [:(NonZero ()),(NonZero ()):] is non empty set
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] 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[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 ()
(0,1) (#) is V11() real ext-real Element of the carrier of ()

bool the carrier of I[01] is non empty set
1 / 2 is V11() real ext-real non negative Element of REAL

the carrier of is non empty set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : b1 `2 <= b1 `1 } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : b1 `1 <= b1 `2 } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : - (b1 `1) <= b1 `2 } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : b1 `2 <= - (b1 `1) } is set

the carrier of is non empty set
[: the carrier of , the carrier of ():] is non empty Relation-like set
bool [: the carrier of , the carrier of ():] 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

proj1 T is 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

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

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]:]
() . 0 is set
() . 1 is set
bool the carrier of 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]

Q is non empty Element of bool the carrier of
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : b1 `2 <= (2 * (b1 `1)) - 1 } is set
AffineMap (1,0,(1 / 2),(1 / 2)) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like V43( the carrier of ()) quasi_total continuous Element of bool [: the carrier of (), the carrier of ():]
Q is Element of bool the carrier of ()
e2 is Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(1 / 2))) .: Q is Element of bool the carrier of ()
gg is set
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of ()
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 ()
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 ()
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 ()
((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 ()
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of ()
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 ()
(AffineMap (1,0,(1 / 2),(1 / 2))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
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 ()
((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 ()
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 () : (2 * (b1 `1)) - 1 <= b1 `2 } is set
Q is Element of bool the carrier of ()
e2 is Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(1 / 2))) .: Q is Element of bool the carrier of ()
gg is set
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of ()
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 ()
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 ()
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 ()
((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 ()
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of ()
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 ()
(AffineMap (1,0,(1 / 2),(1 / 2))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
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 ()
((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 ()
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 () : 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 () -defined the carrier of () -valued Function-like V43( the carrier of ()) quasi_total continuous Element of bool [: the carrier of (), the carrier of ():]
Q is Element of bool the carrier of ()
e2 is Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: Q is Element of bool the carrier of ()
gg is set
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of ()
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 ()
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 ()
(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 ()
((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 ()
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of ()
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 ()
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
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 ()
((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 ()
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 () : b1 `2 <= 1 - (2 * (b1 `1)) } is set
Q is Element of bool the carrier of ()
e2 is Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: Q is Element of bool the carrier of ()
gg is set
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of ()
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 ()
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 ()
(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 ()
((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 ()
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of ()
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 ()
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
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 ()
((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 ()
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

a is V11() real ext-real Element of the carrier of T

a is real-membered SubSpace of T

[: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, the carrier of a:] is non empty Relation-like set
b `2 is set

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

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
b `1 is V11() real ext-real set
a `2 is set
b is Element of the carrier of
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 () : S1[b1] } is set
b is Element of bool the carrier of ()
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(1 / 2))) .: b is Element of bool the carrier of ()
T is closed Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(1 / 2))) " ((AffineMap (1,0,(1 / 2),(1 / 2))) .: b) is Element of bool the carrier of ()
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : S1[b1] } is set
b is Element of bool the carrier of ()
dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(1 / 2))) .: b is Element of bool the carrier of ()
T is closed Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(1 / 2))) " ((AffineMap (1,0,(1 / 2),(1 / 2))) .: b) is Element of bool the carrier of ()
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : S1[b1] } is set
b is Element of bool the carrier of ()
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b is Element of bool the carrier of ()
T is closed Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) " ((AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b) is Element of bool the carrier of ()
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : S1[b1] } is set
b is Element of bool the carrier of ()
dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b is Element of bool the carrier of ()
T is closed Element of bool the carrier of ()
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) " ((AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b) is Element of bool the carrier of ()
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : ( 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 () : S1[b1] } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : S2[b1] } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : ( S2[b1] & S1[b1] ) } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : S2[b1] } /\ { b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : S1[b1] } is set
a is closed Element of bool the carrier of ()
T is closed Element of bool the carrier of ()
a /\ T is closed Element of bool the carrier of ()
REAL 2 is non empty 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

bool is non empty set
[:,(REAL 2):] is non empty Relation-like set
bool [:,(REAL 2):] is non empty set

[: 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 -defined the carrier of () -valued Function-like V43( the carrier of ) quasi_total Element of bool [: the carrier of , the carrier of ():]
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},{b}} is non empty set
a . [b,P] is set
<*b,P*> is set
a . (b,P) is set

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},{b}} is non empty set
a . [b,P] is set
<*b,P*> is set
{ b1 where b1 is Element of the carrier of : b1 `2 <= 1 - (2 * (b1 `1)) } is set
bool the carrier of is non empty set
{ b1 where b1 is Element of the carrier of : S1[b1] } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : S2[b1] } is set
Q is non empty Relation-like the carrier of -defined the carrier of () -valued Function-like V43( the carrier of ) quasi_total Element of bool [: the carrier of , the carrier of ():]
Q is non empty Relation-like the carrier of -defined the carrier of () -valued Function-like V43( the carrier of ) quasi_total Element of bool [: the carrier of , the carrier of ():]
P is Element of bool the carrier of ()
b is Element of bool the carrier of
Q .: b is Element of bool the carrier of ()
Q is set
e2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
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

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},{gg}} is non empty set
g is Element of the carrier of
dom Q is non empty Element of bool the carrier of
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 ()
Q is set
dom Q is non empty Element of bool the carrier of
e2 is set
Q . e2 is set
gg is Element of the carrier of
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 ()
S3 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
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 : b1 `2 <= (2 * (b1 `1)) - 1 } is set
{ b1 where b1 is Element of the carrier of : S1[b1] } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : S2[b1] } is set
Q is non empty Relation-like the carrier of -defined the carrier of () -valued Function-like V43( the carrier of ) quasi_total Element of bool [: the carrier of , the carrier of ():]
Q is non empty Relation-like the carrier of -defined the carrier of () -valued Function-like V43( the carrier of ) quasi_total Element of bool [: the carrier of , the carrier of ():]
P is Element of bool the carrier of ()
b is Element of bool the carrier of
Q .: b is Element of bool the carrier of ()
Q is set
e2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
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

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},{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
dom Q is non empty Element of bool the carrier of
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 ()
Q is set
dom Q is non empty Element of bool the carrier of
e2 is set
Q . e2 is set
gg is Element of the carrier of
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 ()
S3 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
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 : ( 1 - (2 * (b1 `1)) <= b1 `2 & (2 * (b1 `1)) - 1 <= b1 `2 ) } is set
{ b1 where b1 is Element of the carrier of : S1[b1] } is set
{ b1 where b1 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of () : S2[b1] } is set
Q is non empty Relation-like the carrier of -defined the carrier of () -valued Function-like V43( the carrier of ) quasi_total Element of bool [: the carrier of , the carrier of ():]
Q is non empty Relation-like the carrier of -defined the carrier of () -valued Function-like V43( the carrier of ) quasi_total Element of bool [: the carrier of , the carrier of ():]
P is Element of bool the carrier of ()
b is Element of bool the carrier of
Q .: b is Element of bool the carrier of ()
Q is set
e2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
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

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},{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
dom Q is non empty Element of bool the carrier of
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 ()
Q is set
dom Q is non empty Element of bool the carrier of
e2 is set
Q . e2 is set
gg is Element of the carrier of
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 ()
S3 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of ()
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 : b1 `2 <= 1 - (2 * (b1 `1)) } is set
[0,0] is non empty V29() set

is non empty set
P is closed Element of bool the carrier of
[#] is non empty non proper open closed Element of bool the carrier of
P /\ is Element of bool the carrier of
Q is set
e2 is Element of the carrier of
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
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
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
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
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
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 : ( 1 - (2 * (b1 `1)) <= b1 `2 & (2 * (b1 `1)) - 1 <= b1 `2 ) } is set
[1,1] is non empty V29() set

{{1,1},{1}} is non empty set
b is Element of the carrier of
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
[#] is non empty non proper open closed Element of bool the carrier of
P /\ is Element of bool the carrier of
Q is set
e2 is Element of the carrier of
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
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
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
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
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
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 : b1 `2 <= (2 * (b1 `1)) - 1 } is set
[1,0] is non empty V29() set

{{1,0},{1}} is non empty set
P is closed Element of bool the carrier of
[#] is non empty non proper open closed Element of bool the carrier of
P /\ is Element of bool the carrier of
Q is set
e2 is Element of the carrier of
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
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
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
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
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
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

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

[#] () is non proper open closed Element of bool the carrier of ()
the carrier of () is set
bool the carrier of () is non empty set

[#] () is non proper open closed Element of bool the carrier of ()
the carrier of () is set
bool the carrier of () is non empty set
([#] ()) \/ ([#] ()) is set
T \/ ([#] ()) is set
T \/ a is Element of bool the carrier of
[.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

[:{(1 / 2)},[.0,1.]:] is Relation-like set
T is Element of bool the carrier of
a is Element of bool the carrier of

the carrier of () is set

[#] () is non proper open closed Element of bool the carrier of ()
the carrier of () is set
bool the carrier of () is non empty set
[#] () is non proper open closed Element of bool the carrier of ()
bool the carrier of () is non empty set
([#] ()) /\ ([#] ()) is Element of bool the carrier of ()
T /\ ([#] ()) is Element of bool the carrier of ()
T /\ a is Element of bool the carrier of
[.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
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set

T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set

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

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]

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

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

[: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

the carrier of () 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

the carrier of () 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 () -defined the carrier of () -valued Function-like V43( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set
(#) (b,P) is V11() real ext-real Element of the carrier of ()
(b,P) (#) is V11() real ext-real Element of the carrier of ()
L[01] (((#) (b,P)),((b,P) (#))) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like V43( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] 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 () -defined the carrier of () -valued Function-like V43( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] 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 () -defined the carrier of () -valued Function-like V43( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]

the carrier of () is non empty complex-membered ext-real-membered real-membered set

the carrier of () is non empty complex-membered ext-real-membered real-membered set
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set
P[01] (T,a,((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like V43( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set
(#) (b,P) is V11() real ext-real Element of the carrier of ()
(b,P) (#) is V11() real ext-real Element of the carrier of ()
L[01] (((#) (b,P)),((b,P) (#))) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like V43( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] 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 () -defined the carrier of () -valued Function-like V43( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
(T,a,b,P) . T is set
(T,a,b,P) . a is set

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 ()
bool the carrier of () is non empty set
(P[01] (T,a,((#) (0,1)),((0,1) (#)))) . T is set
(L[01] (((#) (b,P)),((b,P) (#)))