:: TOPREAL6 semantic presentation

REAL is non empty non trivial non with_non-empty_elements non finite V202() V203() V204() V208() non bounded_below non bounded_above V280() set
NAT is non empty non with_non-empty_elements epsilon-transitive epsilon-connected ordinal V202() V203() V204() V205() V206() V207() V208() left_end bounded_below Element of bool REAL
bool REAL is non empty set
{} is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set
the empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() real ext-real positive non negative V62() V136() V202() V203() V204() V205() V206() V207() left_end bounded_below Element of NAT
{{},1} is non empty finite V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded set
INT is non empty non trivial non finite V202() V203() V204() V205() V206() V208() set
COMPLEX is non empty non trivial non finite V202() V208() set
omega is non empty non with_non-empty_elements epsilon-transitive epsilon-connected ordinal V202() V203() V204() V205() V206() V207() V208() left_end bounded_below set
bool omega is non empty set
bool NAT is non empty set
K252(NAT) is V61() set
[:1,1:] is non empty RAT -valued INT -valued complex-yielding V193() V194() V195() set
RAT is non empty non trivial non finite V202() V203() V204() V205() V208() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty RAT -valued INT -valued complex-yielding V193() V194() V195() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is non empty complex-yielding V193() V194() set
[:[:REAL,REAL:],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() real ext-real positive non negative V62() V136() V202() V203() V204() V205() V206() V207() left_end bounded_below Element of NAT
[:2,2:] is non empty RAT -valued INT -valued complex-yielding V193() V194() V195() set
[:[:2,2:],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:2,2:],REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
K496() is non empty V151() L10()
the carrier of K496() is non empty set
K501() is non empty V151() V173() V174() V175() V177() V224() V225() V226() V227() V228() V229() L10()
K502() is non empty V151() V175() V177() V227() V228() V229() M17(K501())
K503() is non empty V151() V173() V175() V177() V227() V228() V229() V230() M20(K501(),K502())
K505() is non empty V151() V173() V175() V177() L10()
K506() is non empty V151() V173() V175() V177() V230() M17(K505())
TOP-REAL 2 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
bool the carrier of (TOP-REAL 2) is non empty set
[: the carrier of (TOP-REAL 2),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of (TOP-REAL 2),REAL:] is non empty set
I[01] is non empty strict TopSpace-like V270() TopStruct
the carrier of I[01] is non empty V202() V203() V204() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V270() MetrStruct
R^1 is non empty strict TopSpace-like V270() TopStruct
the carrier of R^1 is non empty V202() V203() V204() set
[:COMPLEX,COMPLEX:] is non empty complex-yielding set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is non empty complex-yielding V193() V194() set
bool [:COMPLEX,REAL:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:RAT,RAT:] is non empty RAT -valued complex-yielding V193() V194() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty RAT -valued complex-yielding V193() V194() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty RAT -valued INT -valued complex-yielding V193() V194() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty RAT -valued INT -valued complex-yielding V193() V194() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty RAT -valued INT -valued complex-yielding V193() V194() V195() set
[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued complex-yielding V193() V194() V195() set
bool [:[:NAT,NAT:],NAT:] is non empty set
ExtREAL is non empty V203() V280() set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V31() real ext-real positive non negative V62() V136() V202() V203() V204() V205() V206() V207() left_end bounded_below Element of NAT
0 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V62() V136() V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of NAT
absreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:REAL,REAL:]
Seg 1 is non empty finite V43(1) V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{1} is non empty finite V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded set
Seg 2 is non empty finite V43(2) V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{1,2} is non empty finite V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded set
bool the carrier of R^1 is non empty set
[:NAT,REAL:] is non empty complex-yielding V193() V194() set
bool [:NAT,REAL:] is non empty set
proj1 is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]
proj2 is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:REAL,REAL:]
<*> REAL is empty proper Relation-like NAT -defined REAL -valued Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V193() V194() V195() V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() FinSequence of REAL
Product (<*> REAL) is V31() real ext-real Element of REAL
sqrt 2 is V31() real ext-real Element of REAL
TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct
R^2-unit_square is being_special_polygon non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
|[0,0]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|[0,1]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,0]|,|[0,1]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * |[0,0]|) + (b₁ * |[0,1]|)) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
|[1,1]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,1]|,|[1,1]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * |[0,1]|) + (b₁ * |[1,1]|)) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is non empty Element of bool the carrier of (TOP-REAL 2)
|[1,0]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg (|[1,1]|,|[1,0]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * |[1,1]|) + (b₁ * |[1,0]|)) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (|[1,0]|,|[0,0]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * |[1,0]|) + (b₁ * |[0,0]|)) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)) is non empty Element of bool the carrier of (TOP-REAL 2)
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is non empty Element of bool the carrier of (TOP-REAL 2)
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is Element of bool the carrier of (TOP-REAL 2)
{|[0,1]|} is non empty finite V40() set
LSeg (|[0,0]|,|[1,0]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * |[0,0]|) + (b₁ * |[1,0]|)) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (|[1,0]|,|[1,1]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * |[1,0]|) + (b₁ * |[1,1]|)) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is Element of bool the carrier of (TOP-REAL 2)
{|[1,0]|} is non empty finite V40() set
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is Element of bool the carrier of (TOP-REAL 2)
{|[1,1]|} is non empty finite V40() set
Euclid 2 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL 2 is non empty functional FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 2 } is set
Pitag_dist 2 is non empty Relation-like [:(REAL 2),(REAL 2):] -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:[:(REAL 2),(REAL 2):],REAL:]
[:(REAL 2),(REAL 2):] is non empty set
[:[:(REAL 2),(REAL 2):],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:(REAL 2),(REAL 2):],REAL:] is non empty set
MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct
the carrier of (Euclid 2) is non empty set
union {} is epsilon-transitive epsilon-connected ordinal finite set
x1 is V31() real ext-real set
x2 is V31() real ext-real set
x1 + x2 is V31() real ext-real set
sqrt (x1 + x2) is V31() real ext-real set
sqrt x1 is V31() real ext-real set
sqrt x2 is V31() real ext-real set
(sqrt x1) + (sqrt x2) is V31() real ext-real set
x1 is V31() real ext-real set
abs x1 is V31() real ext-real Element of REAL
x2 is V31() real ext-real set
abs x2 is V31() real ext-real Element of REAL
x1 is V31() real ext-real set
abs x1 is V31() real ext-real Element of REAL
x2 is V31() real ext-real set
abs x2 is V31() real ext-real Element of REAL
- x2 is V31() real ext-real set
- x1 is V31() real ext-real set
x1 is V31() real ext-real Element of REAL
0 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 0 -tuples_on REAL
0 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 0 } is set
Seg 0 is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() V43( 0 ) FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool NAT
(Seg 0) --> x1 is empty Relation-like Seg 0 -defined {x1} -valued Function-like functional total quasi_total epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V193() V194() V195() V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool [:(Seg 0),{x1}:]
{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
[:(Seg 0),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg 0),{x1}:] is non empty finite V40() set
Product (0 |-> x1) is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
1 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 1 -tuples_on REAL
1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 1 } is set
(Seg 1) --> x1 is non empty Relation-like Seg 1 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg 1),{x1}:]
{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
[:(Seg 1),{x1}:] is non empty finite complex-yielding V193() V194() set
bool [:(Seg 1),{x1}:] is non empty finite V40() set
Product (1 |-> x1) is V31() real ext-real Element of REAL
<*x1*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(1) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
Product <*x1*> is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 2 -tuples_on REAL
(Seg 2) --> x1 is non empty Relation-like Seg 2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg 2),{x1}:]
{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
[:(Seg 2),{x1}:] is non empty finite complex-yielding V193() V194() set
bool [:(Seg 2),{x1}:] is non empty finite V40() set
Product (2 |-> x1) is V31() real ext-real Element of REAL
x1 * x1 is V31() real ext-real Element of REAL
<*x1,x1*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
Product <*x1,x1*> is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
x2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
(x2 + 1) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (x2 + 1) -tuples_on REAL
(x2 + 1) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = x2 + 1 } is set
Seg (x2 + 1) is finite V43(x2 + 1) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg (x2 + 1)) --> x1 is Relation-like Seg (x2 + 1) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (x2 + 1)),{x1}:]
{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
[:(Seg (x2 + 1)),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg (x2 + 1)),{x1}:] is non empty finite V40() set
Product ((x2 + 1) |-> x1) is V31() real ext-real Element of REAL
x2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of x2 -tuples_on REAL
x2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = x2 } is set
Seg x2 is finite V43(x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg x2) --> x1 is Relation-like Seg x2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg x2),{x1}:]
[:(Seg x2),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg x2),{x1}:] is non empty finite V40() set
Product (x2 |-> x1) is V31() real ext-real Element of REAL
(Product (x2 |-> x1)) * x1 is V31() real ext-real Element of REAL
1 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 1 -tuples_on REAL
1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 1 } is set
(Seg 1) --> x1 is non empty Relation-like Seg 1 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg 1),{x1}:]
[:(Seg 1),{x1}:] is non empty finite complex-yielding V193() V194() set
bool [:(Seg 1),{x1}:] is non empty finite V40() set
Product (1 |-> x1) is V31() real ext-real Element of REAL
(Product (x2 |-> x1)) * (Product (1 |-> x1)) is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
x2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of x2 -tuples_on REAL
x2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = x2 } is set
Seg x2 is finite V43(x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg x2) --> x1 is Relation-like Seg x2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg x2),{x1}:]
{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
[:(Seg x2),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg x2),{x1}:] is non empty finite V40() set
Product (x2 |-> x1) is V31() real ext-real Element of REAL
dom (x2 |-> x1) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
y2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real set
y2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
(x2 |-> x1) . 1 is V31() real ext-real Element of REAL
y2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real set
(x2 |-> x1) . y2 is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
x2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of x2 -tuples_on REAL
x2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = x2 } is set
Seg x2 is finite V43(x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg x2) --> x1 is Relation-like Seg x2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg x2),{x1}:]
{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
[:(Seg x2),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg x2),{x1}:] is non empty finite V40() set
Product (x2 |-> x1) is V31() real ext-real Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
y1 -' x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real non negative V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
(y1 -' x2) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (y1 -' x2) -tuples_on REAL
(y1 -' x2) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = y1 -' x2 } is set
Seg (y1 -' x2) is finite V43(y1 -' x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg (y1 -' x2)) --> x1 is Relation-like Seg (y1 -' x2) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (y1 -' x2)),{x1}:]
[:(Seg (y1 -' x2)),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg (y1 -' x2)),{x1}:] is non empty finite V40() set
Product ((y1 -' x2) |-> x1) is V31() real ext-real Element of REAL
y1 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of y1 -tuples_on REAL
y1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = y1 } is set
Seg y1 is finite V43(y1) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg y1) --> x1 is Relation-like Seg y1 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg y1),{x1}:]
[:(Seg y1),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg y1),{x1}:] is non empty finite V40() set
Product (y1 |-> x1) is V31() real ext-real Element of REAL
(Product (y1 |-> x1)) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL
y2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
y2 -' x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real non negative V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
(y2 -' x2) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (y2 -' x2) -tuples_on REAL
(y2 -' x2) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = y2 -' x2 } is set
Seg (y2 -' x2) is finite V43(y2 -' x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg (y2 -' x2)) --> x1 is Relation-like Seg (y2 -' x2) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (y2 -' x2)),{x1}:]
[:(Seg (y2 -' x2)),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg (y2 -' x2)),{x1}:] is non empty finite V40() set
Product ((y2 -' x2) |-> x1) is V31() real ext-real Element of REAL
y2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of y2 -tuples_on REAL
y2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = y2 } is set
Seg y2 is finite V43(y2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg y2) --> x1 is Relation-like Seg y2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg y2),{x1}:]
[:(Seg y2),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg y2),{x1}:] is non empty finite V40() set
Product (y2 |-> x1) is V31() real ext-real Element of REAL
(Product (y2 |-> x1)) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL
y2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
(y2 + 1) -' x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real non negative V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
((y2 + 1) -' x2) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of ((y2 + 1) -' x2) -tuples_on REAL
((y2 + 1) -' x2) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = (y2 + 1) -' x2 } is set
Seg ((y2 + 1) -' x2) is finite V43((y2 + 1) -' x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg ((y2 + 1) -' x2)) --> x1 is Relation-like Seg ((y2 + 1) -' x2) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg ((y2 + 1) -' x2)),{x1}:]
[:(Seg ((y2 + 1) -' x2)),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg ((y2 + 1) -' x2)),{x1}:] is non empty finite V40() set
Product (((y2 + 1) -' x2) |-> x1) is V31() real ext-real Element of REAL
(y2 + 1) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (y2 + 1) -tuples_on REAL
(y2 + 1) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = y2 + 1 } is set
Seg (y2 + 1) is finite V43(y2 + 1) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg (y2 + 1)) --> x1 is Relation-like Seg (y2 + 1) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (y2 + 1)),{x1}:]
[:(Seg (y2 + 1)),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg (y2 + 1)),{x1}:] is non empty finite V40() set
Product ((y2 + 1) |-> x1) is V31() real ext-real Element of REAL
(Product ((y2 + 1) |-> x1)) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL
(y2 -' x2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() real ext-real positive non negative V62() V136() V202() V203() V204() V205() V206() V207() left_end bounded_below Element of NAT
((y2 -' x2) + 1) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of ((y2 -' x2) + 1) -tuples_on REAL
((y2 -' x2) + 1) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = (y2 -' x2) + 1 } is set
Seg ((y2 -' x2) + 1) is non empty finite V43((y2 -' x2) + 1) V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
(Seg ((y2 -' x2) + 1)) --> x1 is non empty Relation-like Seg ((y2 -' x2) + 1) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg ((y2 -' x2) + 1)),{x1}:]
[:(Seg ((y2 -' x2) + 1)),{x1}:] is non empty finite complex-yielding V193() V194() set
bool [:(Seg ((y2 -' x2) + 1)),{x1}:] is non empty finite V40() set
Product (((y2 -' x2) + 1) |-> x1) is V31() real ext-real Element of REAL
1 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 1 -tuples_on REAL
1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 1 } is set
(Seg 1) --> x1 is non empty Relation-like Seg 1 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg 1),{x1}:]
[:(Seg 1),{x1}:] is non empty finite complex-yielding V193() V194() set
bool [:(Seg 1),{x1}:] is non empty finite V40() set
Product (1 |-> x1) is V31() real ext-real Element of REAL
(Product ((y2 -' x2) |-> x1)) * (Product (1 |-> x1)) is V31() real ext-real Element of REAL
((Product (y2 |-> x1)) / (Product (x2 |-> x1))) * x1 is V31() real ext-real Element of REAL
(Product (y2 |-> x1)) * x1 is V31() real ext-real Element of REAL
((Product (y2 |-> x1)) * x1) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL
0 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 0 -tuples_on REAL
0 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 0 } is set
Seg 0 is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() V43( 0 ) FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool NAT
(Seg 0) --> x1 is empty Relation-like Seg 0 -defined {x1} -valued Function-like functional total quasi_total epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V193() V194() V195() V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool [:(Seg 0),{x1}:]
[:(Seg 0),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg 0),{x1}:] is non empty finite V40() set
Product (0 |-> x1) is V31() real ext-real Element of REAL
0 -' x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real non negative V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
(0 -' x2) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (0 -' x2) -tuples_on REAL
(0 -' x2) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 0 -' x2 } is set
Seg (0 -' x2) is finite V43(0 -' x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg (0 -' x2)) --> x1 is Relation-like Seg (0 -' x2) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (0 -' x2)),{x1}:]
[:(Seg (0 -' x2)),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg (0 -' x2)),{x1}:] is non empty finite V40() set
Product ((0 -' x2) |-> x1) is V31() real ext-real Element of REAL
0 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 0 -tuples_on REAL
0 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 0 } is set
Seg 0 is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() V43( 0 ) FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool NAT
(Seg 0) --> x1 is empty Relation-like Seg 0 -defined {x1} -valued Function-like functional total quasi_total epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V193() V194() V195() V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool [:(Seg 0),{x1}:]
[:(Seg 0),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg 0),{x1}:] is non empty finite V40() set
Product (0 |-> x1) is V31() real ext-real Element of REAL
(Product (0 |-> x1)) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL
(Product (0 |-> x1)) / (Product (<*> REAL)) is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
x1 |^ x2 is V31() real ext-real Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
y1 -' x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real non negative V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
x1 |^ (y1 -' x2) is V31() real ext-real Element of REAL
x1 |^ y1 is V31() real ext-real Element of REAL
(x1 |^ y1) / (x1 |^ x2) is V31() real ext-real Element of REAL
y1 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of y1 -tuples_on REAL
y1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = y1 } is set
Seg y1 is finite V43(y1) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg y1) --> x1 is Relation-like Seg y1 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg y1),{x1}:]
{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
[:(Seg y1),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg y1),{x1}:] is non empty finite V40() set
Product (y1 |-> x1) is V31() real ext-real Element of REAL
(Product (y1 |-> x1)) / (x1 |^ x2) is V31() real ext-real Element of REAL
x2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of x2 -tuples_on REAL
x2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = x2 } is set
Seg x2 is finite V43(x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg x2) --> x1 is Relation-like Seg x2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg x2),{x1}:]
[:(Seg x2),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg x2),{x1}:] is non empty finite V40() set
Product (x2 |-> x1) is V31() real ext-real Element of REAL
(Product (y1 |-> x1)) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL
(y1 -' x2) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (y1 -' x2) -tuples_on REAL
(y1 -' x2) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = y1 -' x2 } is set
Seg (y1 -' x2) is finite V43(y1 -' x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
(Seg (y1 -' x2)) --> x1 is Relation-like Seg (y1 -' x2) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (y1 -' x2)),{x1}:]
[:(Seg (y1 -' x2)),{x1}:] is finite complex-yielding V193() V194() set
bool [:(Seg (y1 -' x2)),{x1}:] is non empty finite V40() set
Product ((y1 -' x2) |-> x1) is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
x1 ^2 is V31() real ext-real Element of REAL
x1 * x1 is V31() real ext-real set
x2 is V31() real ext-real Element of REAL
<*x1,x2*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
sqr <*x1,x2*> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
x2 ^2 is V31() real ext-real Element of REAL
x2 * x2 is V31() real ext-real set
<*(x1 ^2),(x2 ^2)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
dom sqrreal is V202() V203() V204() Element of bool REAL
rng <*x1,x2*> is finite compact closed V202() V203() V204() bounded_below bounded_above real-bounded Element of bool REAL
dom <*(x1 ^2),(x2 ^2)*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
y1 is set
(sqr <*x1,x2*>) . y1 is V31() real ext-real Element of REAL
<*(x1 ^2),(x2 ^2)*> . y1 is V31() real ext-real Element of REAL
<*x1,x2*> . 1 is V31() real ext-real Element of REAL
<*x1,x2*> . 2 is V31() real ext-real Element of REAL
dom (sqr <*x1,x2*>) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
sqrreal * <*x1,x2*> is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding V193() V194() Element of bool [:NAT,REAL:]
dom (sqrreal * <*x1,x2*>) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
dom <*x1,x2*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
x1 is V31() real ext-real Element of REAL
abs x1 is V31() real ext-real Element of REAL
x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real set
y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
abs y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
y1 * absreal is Relation-like finite complex-yielding V193() V194() set
dom (abs y1) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
y1 . x2 is V31() real ext-real Element of REAL
(abs y1) . x2 is V31() real ext-real Element of REAL
absreal . x1 is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
abs x1 is V31() real ext-real Element of REAL
x2 is V31() real ext-real Element of REAL
<*x1,x2*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
abs <*x1,x2*> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
<*x1,x2*> * absreal is Relation-like finite complex-yielding V193() V194() set
abs x2 is V31() real ext-real Element of REAL
<*(abs x1),(abs x2)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
dom absreal is V202() V203() V204() Element of bool REAL
rng <*x1,x2*> is finite compact closed V202() V203() V204() bounded_below bounded_above real-bounded Element of bool REAL
dom (abs <*x1,x2*>) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
dom <*x1,x2*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
dom <*(abs x1),(abs x2)*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
y1 is set
(abs <*x1,x2*>) . y1 is V31() real ext-real Element of REAL
<*(abs x1),(abs x2)*> . y1 is V31() real ext-real Element of REAL
<*x1,x2*> . 1 is V31() real ext-real Element of REAL
<*x1,x2*> . 2 is V31() real ext-real Element of REAL
x1 is V31() real ext-real set
x2 is V31() real ext-real set
y1 is V31() real ext-real set
y2 is V31() real ext-real set
x2 - x1 is V31() real ext-real set
abs (x2 - x1) is V31() real ext-real Element of REAL
y2 - y1 is V31() real ext-real set
abs (y2 - y1) is V31() real ext-real Element of REAL
(abs (x2 - x1)) + (abs (y2 - y1)) is V31() real ext-real Element of REAL
(x2 - x1) + (y2 - y1) is V31() real ext-real set
x1 - x1 is V31() real ext-real set
y1 - y1 is V31() real ext-real set
x2 is V31() real ext-real set
x1 is V31() real ext-real set
x1 - x2 is V31() real ext-real set
x1 + x2 is V31() real ext-real set
].(x1 - x2),(x1 + x2).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
x1 - x1 is V31() real ext-real set
abs (x1 - x1) is V31() real ext-real Element of REAL
x2 is V31() real ext-real set
x1 is V31() real ext-real set
x1 - x2 is V31() real ext-real set
x1 + x2 is V31() real ext-real set
[.(x1 - x2),(x1 + x2).] is compact closed V202() V203() V204() bounded_below bounded_above real-bounded V280() Element of bool REAL
y1 is V31() real ext-real Element of REAL
y1 + 0 is V31() real ext-real Element of REAL
y2 is V31() real ext-real Element of REAL
y1 + y2 is V31() real ext-real Element of REAL
y1 - y2 is V31() real ext-real Element of REAL
[.(y1 - y2),(y1 + y2).] is compact closed V202() V203() V204() bounded_below bounded_above real-bounded V280() Element of bool REAL
{ b₁ where b₁ is V31() real ext-real Element of REAL : ( y1 - y2 <= b₁ & b₁ <= y1 + y2 ) } is set
y1 - 0 is V31() real ext-real Element of REAL
x2 is V31() real ext-real set
x1 is V31() real ext-real set
].x1,x2.[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
lower_bound ].x1,x2.[ is V31() real ext-real Element of REAL
upper_bound ].x1,x2.[ is V31() real ext-real Element of REAL
a is V31() real ext-real Element of REAL
y2 is V31() real ext-real Element of REAL
y2 + a is V31() real ext-real Element of REAL
(y2 + a) / 2 is V31() real ext-real Element of REAL
{ b₁ where b₁ is V31() real ext-real Element of REAL : ( not b₁ <= y2 & not a <= b₁ ) } is set
b is V31() real ext-real set
y2 + b is V31() real ext-real Element of REAL
O is V31() real ext-real Element of REAL
y2 + O is V31() real ext-real Element of REAL
O is V31() real ext-real Element of REAL
y2 + O is V31() real ext-real Element of REAL
y2 + (y2 + O) is V31() real ext-real Element of REAL
(y2 + (y2 + O)) / 2 is V31() real ext-real Element of REAL
O is V31() real ext-real Element of REAL
y2 + O is V31() real ext-real Element of REAL
b is V31() real ext-real set
a - b is V31() real ext-real Element of REAL
O is V31() real ext-real Element of REAL
a - O is V31() real ext-real Element of REAL
O is V31() real ext-real Element of REAL
a - O is V31() real ext-real Element of REAL
a - 0 is V31() real ext-real Element of REAL
a + (a - O) is V31() real ext-real Element of REAL
(a + (a - O)) / 2 is V31() real ext-real Element of REAL
O is V31() real ext-real Element of REAL
a - O is V31() real ext-real Element of REAL
b is ext-real set
O is V31() real ext-real Element of REAL
b is V31() real ext-real set
O is V31() real ext-real Element of REAL
b is ext-real set
O is V31() real ext-real Element of REAL
b is V31() real ext-real set
O is V31() real ext-real Element of REAL
x1 is TopStruct
the carrier of x1 is set
bool the carrier of x1 is non empty set
x2 is finite Element of bool the carrier of x1
x1 | x2 is strict SubSpace of x1
x1 is TopStruct
the carrier of x1 is set
bool the carrier of x1 is non empty set
x2 is Element of bool the carrier of x1
x1 | x2 is strict SubSpace of x1
the carrier of (x1 | x2) is set
bool the carrier of (x1 | x2) is non empty set
[#] (x1 | x2) is non proper dense Element of bool the carrier of (x1 | x2)
y2 is Element of bool the carrier of (x1 | x2)
a is Element of bool the carrier of (x1 | x2)
y2 \/ a is Element of bool the carrier of (x1 | x2)
{} (x1 | x2) is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered boundary compact V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool the carrier of (x1 | x2)
y1 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered boundary compact V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool the carrier of x1
x1 | y1 is empty trivial finite {} -element strict T_0 T_1 T_2 SubSpace of x1
[#] (x1 | y1) is empty trivial non proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered dense boundary compact V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool the carrier of (x1 | y1)
the carrier of (x1 | y1) is empty trivial functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set
bool the carrier of (x1 | y1) is non empty finite V40() set
x1 is TopSpace-like TopStruct
x2 is TopSpace-like TopStruct
the carrier of x1 is set
the carrier of x2 is set
[: the carrier of x1, the carrier of x2:] is set
bool [: the carrier of x1, the carrier of x2:] is non empty set
y1 is Relation-like the carrier of x1 -defined the carrier of x2 -valued Function-like quasi_total Element of bool [: the carrier of x1, the carrier of x2:]
rng y1 is Element of bool the carrier of x2
bool the carrier of x2 is non empty set
[#] x2 is non proper open closed dense Element of bool the carrier of x2
dom y1 is Element of bool the carrier of x1
bool the carrier of x1 is non empty set
[#] x1 is non proper open closed dense Element of bool the carrier of x1
y1 .: ([#] x1) is Element of bool the carrier of x2
x1 is TopSpace-like TopStruct
the carrier of x1 is set
bool the carrier of x1 is non empty set
bool (bool the carrier of x1) is non empty set
x2 is finite Element of bool (bool the carrier of x1)
union x2 is Element of bool the carrier of x1
y1 is set
y2 is set
union y2 is set
{y1} is non empty finite set
y2 \/ {y1} is non empty set
union (y2 \/ {y1}) is set
bool the carrier of x1 is non empty Element of bool (bool the carrier of x1)
a is set
O is Element of bool the carrier of x1
a is Element of bool (bool the carrier of x1)
union a is Element of bool the carrier of x1
b is Element of bool the carrier of x1
(union a) \/ b is Element of bool the carrier of x1
union {y1} is set
{} x1 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered open closed boundary nowhere_dense connected compact V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool the carrier of x1
union x2 is set
y1 is Element of bool the carrier of x1
x1 is set
x2 is set
y1 is set
y2 is set
a is set
b is set
(a,b) --> (x1,y1) is Relation-like Function-like finite set
product ((a,b) --> (x1,y1)) is set
(a,b) --> (x2,y2) is Relation-like Function-like finite set
product ((a,b) --> (x2,y2)) is set
dom ((a,b) --> (x1,y1)) is finite set
{a,b} is non empty finite set
g is set
((a,b) --> (x1,y1)) . g is set
((a,b) --> (x2,y2)) . g is set
((a,b) --> (x1,y1)) . b is set
((a,b) --> (x1,y1)) . a is set
a .--> y1 is trivial finite set
((a,b) --> (x1,y1)) . a is set
a .--> y2 is trivial finite set
dom ((a,b) --> (x2,y2)) is finite set
x1 is V202() V203() V204() Element of bool REAL
x2 is V202() V203() V204() Element of bool REAL
(1,2) --> (x1,x2) is non empty Relation-like NAT -defined {1,2} -defined bool REAL -valued Function-like total quasi_total finite Element of bool [:{1,2},(bool REAL):]
[:{1,2},(bool REAL):] is non empty set
bool [:{1,2},(bool REAL):] is non empty set
product ((1,2) --> (x1,x2)) is set
y2 is set
((1,2) --> (x1,x2)) . 1 is set
((1,2) --> (x1,x2)) . 2 is set
dom ((1,2) --> (x1,x2)) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool {1,2}
bool {1,2} is non empty finite V40() set
a is Relation-like Function-like set
dom a is set
a . 2 is set
a . 1 is set
g is set
a . g is set
<*(a . 1),(a . 2)*> is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like set
<*(a . 1),(a . 2)*> . g is set
dom <*(a . 1),(a . 2)*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
b is V31() real ext-real Element of REAL
O is V31() real ext-real Element of REAL
|[b,O]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 is V31() real ext-real Element of REAL
|[0,x1]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|.|[0,x1]|.| is V31() real ext-real non negative Element of REAL
sqr |[0,x1]| is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
Sum (sqr |[0,x1]|) is V31() real ext-real Element of REAL
sqrt (Sum (sqr |[0,x1]|)) is V31() real ext-real Element of REAL
abs x1 is V31() real ext-real Element of REAL
|[x1,0]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|.|[x1,0]|.| is V31() real ext-real non negative Element of REAL
sqr |[x1,0]| is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
Sum (sqr |[x1,0]|) is V31() real ext-real Element of REAL
sqrt (Sum (sqr |[x1,0]|)) is V31() real ext-real Element of REAL
<*0,x1*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
|.<*0,x1*>.| is V31() real ext-real non negative Element of REAL
sqr <*0,x1*> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
Sum (sqr <*0,x1*>) is V31() real ext-real Element of REAL
sqrt (Sum (sqr <*0,x1*>)) is V31() real ext-real Element of REAL
0 ^2 is V31() real ext-real Element of REAL
0 * 0 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set
x1 ^2 is V31() real ext-real Element of REAL
x1 * x1 is V31() real ext-real set
<*(0 ^2),(x1 ^2)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
Sum <*(0 ^2),(x1 ^2)*> is V31() real ext-real Element of REAL
sqrt (Sum <*(0 ^2),(x1 ^2)*>) is V31() real ext-real Element of REAL
0 + (x1 ^2) is V31() real ext-real Element of REAL
sqrt (0 + (x1 ^2)) is V31() real ext-real Element of REAL
<*x1,0*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
|.<*x1,0*>.| is V31() real ext-real non negative Element of REAL
sqr <*x1,0*> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
Sum (sqr <*x1,0*>) is V31() real ext-real Element of REAL
sqrt (Sum (sqr <*x1,0*>)) is V31() real ext-real Element of REAL
<*(x1 ^2),(0 ^2)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
Sum <*(x1 ^2),(0 ^2)*> is V31() real ext-real Element of REAL
sqrt (Sum <*(x1 ^2),(0 ^2)*>) is V31() real ext-real Element of REAL
(x1 ^2) + 0 is V31() real ext-real Element of REAL
sqrt ((x1 ^2) + 0) is V31() real ext-real Element of REAL
0. (TOP-REAL 2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like V72( TOP-REAL 2) complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
<*0,0*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() V195() FinSequence of NAT
x1 is Element of the carrier of (Euclid 2)
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 `1 is V31() real ext-real Element of REAL
x2 . 1 is V31() real ext-real Element of REAL
x2 `2 is V31() real ext-real Element of REAL
x2 . 2 is V31() real ext-real Element of REAL
0.REAL 2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
2 |-> 0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 2 -tuples_on REAL
(Seg 2) --> 0 is non empty Relation-like Seg 2 -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite complex-yielding V193() V194() V195() Element of bool [:(Seg 2),{0}:]
{0} is non empty finite V40() V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded set
[:(Seg 2),{0}:] is non empty INT -valued RAT -valued finite complex-yielding V193() V194() V195() set
bool [:(Seg 2),{0}:] is non empty finite V40() set
0.REAL 2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
2 |-> 0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 2 -tuples_on REAL
(Seg 2) --> 0 is non empty Relation-like Seg 2 -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite complex-yielding V193() V194() V195() Element of bool [:(Seg 2),{0}:]
{0} is non empty finite V40() V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded set
[:(Seg 2),{0}:] is non empty INT -valued RAT -valued finite complex-yielding V193() V194() V195() set
bool [:(Seg 2),{0}:] is non empty finite V40() set
x1 is Element of the carrier of (Euclid 2)
x2 is Element of the carrier of (Euclid 2)
dist (x1,x2) is V31() real ext-real Element of REAL
y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|.y1.| is V31() real ext-real non negative Element of REAL
sqr y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
Sum (sqr y1) is V31() real ext-real Element of REAL
sqrt (Sum (sqr y1)) is V31() real ext-real Element of REAL
y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y2 `1 is V31() real ext-real Element of REAL
y2 . 1 is V31() real ext-real Element of REAL
y2 `2 is V31() real ext-real Element of REAL
y2 . 2 is V31() real ext-real Element of REAL
(Pitag_dist 2) . (x1,x2) is set
[x1,x2] is set
{x1,x2} is non empty finite set
{x1} is non empty finite set
{{x1,x2},{x1}} is non empty finite V40() set
(Pitag_dist 2) . [x1,x2] is V31() real ext-real set
y1 `1 is V31() real ext-real Element of REAL
y1 . 1 is V31() real ext-real Element of REAL
(y2 `1) - (y1 `1) is V31() real ext-real Element of REAL
((y2 `1) - (y1 `1)) ^2 is V31() real ext-real Element of REAL
((y2 `1) - (y1 `1)) * ((y2 `1) - (y1 `1)) is V31() real ext-real set
y1 `2 is V31() real ext-real Element of REAL
y1 . 2 is V31() real ext-real Element of REAL
(y2 `2) - (y1 `2) is V31() real ext-real Element of REAL
((y2 `2) - (y1 `2)) ^2 is V31() real ext-real Element of REAL
((y2 `2) - (y1 `2)) * ((y2 `2) - (y1 `2)) is V31() real ext-real set
(((y2 `1) - (y1 `1)) ^2) + (((y2 `2) - (y1 `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((y2 `1) - (y1 `1)) ^2) + (((y2 `2) - (y1 `2)) ^2)) is V31() real ext-real Element of REAL
(y1 `1) ^2 is V31() real ext-real Element of REAL
(y1 `1) * (y1 `1) is V31() real ext-real set
(y1 `2) ^2 is V31() real ext-real Element of REAL
(y1 `2) * (y1 `2) is V31() real ext-real set
((y1 `1) ^2) + ((y1 `2) ^2) is V31() real ext-real Element of REAL
sqrt (((y1 `1) ^2) + ((y1 `2) ^2)) is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 * x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 * x2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
x2 `1 is V31() real ext-real Element of REAL
x2 . 1 is V31() real ext-real Element of REAL
x1 * (x2 `1) is V31() real ext-real Element of REAL
x2 `2 is V31() real ext-real Element of REAL
x2 . 2 is V31() real ext-real Element of REAL
x1 * (x2 `2) is V31() real ext-real Element of REAL
|[(x1 * (x2 `1)),(x1 * (x2 `2))]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|[(x2 `1),(x2 `2)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 is V31() real ext-real Element of REAL
1 - x1 is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(1 - x1) * y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(1 - x1) * y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 * y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 * y2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
((1 - x1) * y1) + (x1 * y2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - x1) * y1) + (x1 * y2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
1 - 0 is non empty V31() real ext-real positive non negative Element of REAL
(1 - 0) * y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(1 - 0) * y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
((1 - 0) * y1) + (x1 * y2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - 0) * y1) + (x1 * y2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
0 * y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
0 * y2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
((1 - 0) * y1) + (0 * y2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - 0) * y1) + (0 * y2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
1 * y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
1 * y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
(1 * y1) + (0. (TOP-REAL 2)) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(1 * y1) + (0. (TOP-REAL 2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
x1 is V31() real ext-real Element of REAL
1 - x1 is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(1 - x1) * y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(1 - x1) * y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 * y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 * y2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
((1 - x1) * y1) + (x1 * y2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - x1) * y1) + (x1 * y2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
1 - 1 is V31() real ext-real Element of REAL
(1 - 1) * y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(1 - 1) * y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
((1 - 1) * y1) + (x1 * y2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - 1) * y1) + (x1 * y2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
0 * y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
0 * y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
1 * y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
1 * y2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
(0 * y1) + (1 * y2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(0 * y1) + (1 * y2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
(0. (TOP-REAL 2)) + (1 * y2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(0. (TOP-REAL 2)) + (1 * y2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `1 is V31() real ext-real Element of REAL
x1 . 1 is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 `1 is V31() real ext-real Element of REAL
x2 . 1 is V31() real ext-real Element of REAL
y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg (x2,y1) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * x2) + (b₁ * y1)) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
y1 `1 is V31() real ext-real Element of REAL
y1 . 1 is V31() real ext-real Element of REAL
(x2 `1) - (y1 `1) is V31() real ext-real Element of REAL
y2 is V31() real ext-real Element of REAL
1 - y2 is V31() real ext-real Element of REAL
(1 - y2) * x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(1 - y2) * x2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
y2 * y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y2 * y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
((1 - y2) * x2) + (y2 * y1) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - y2) * x2) + (y2 * y1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
(1 - y2) * (x2 `1) is V31() real ext-real Element of REAL
x2 `2 is V31() real ext-real Element of REAL
x2 . 2 is V31() real ext-real Element of REAL
(1 - y2) * (x2 `2) is V31() real ext-real Element of REAL
|[((1 - y2) * (x2 `1)),((1 - y2) * (x2 `2))]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - y2) * x2) `1 is V31() real ext-real Element of REAL
((1 - y2) * x2) . 1 is V31() real ext-real Element of REAL
y2 * (y1 `1) is V31() real ext-real Element of REAL
y1 `2 is V31() real ext-real Element of REAL
y1 . 2 is V31() real ext-real Element of REAL
y2 * (y1 `2) is V31() real ext-real Element of REAL
|[(y2 * (y1 `1)),(y2 * (y1 `2))]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(y2 * y1) `1 is V31() real ext-real Element of REAL
(y2 * y1) . 1 is V31() real ext-real Element of REAL
(((1 - y2) * x2) `1) + ((y2 * y1) `1) is V31() real ext-real Element of REAL
((1 - y2) * x2) `2 is V31() real ext-real Element of REAL
((1 - y2) * x2) . 2 is V31() real ext-real Element of REAL
(y2 * y1) `2 is V31() real ext-real Element of REAL
(y2 * y1) . 2 is V31() real ext-real Element of REAL
(((1 - y2) * x2) `2) + ((y2 * y1) `2) is V31() real ext-real Element of REAL
|[((((1 - y2) * x2) `1) + ((y2 * y1) `1)),((((1 - y2) * x2) `2) + ((y2 * y1) `2))]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - y2) * (x2 `1)) + (y2 * (y1 `1)) is V31() real ext-real Element of REAL
(x2 `1) - (x1 `1) is V31() real ext-real Element of REAL
y2 * ((x2 `1) - (y1 `1)) is V31() real ext-real Element of REAL
(y1 `1) - (x2 `1) is V31() real ext-real Element of REAL
(y1 `1) - (x1 `1) is V31() real ext-real Element of REAL
(1 - y2) * ((y1 `1) - (x2 `1)) is V31() real ext-real Element of REAL
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `2 is V31() real ext-real Element of REAL
x1 . 2 is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 `2 is V31() real ext-real Element of REAL
x2 . 2 is V31() real ext-real Element of REAL
y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg (x2,y1) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b<sub>1</sub>) * x2) + (b<sub>1</sub> * y1)) where b<sub>1</sub> is V31() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
y1 `2 is V31() real ext-real Element of REAL
y1 . 2 is V31() real ext-real Element of REAL
(x2 `2) - (y1 `2) is V31() real ext-real Element of REAL
y2 is V31() real ext-real Element of REAL
1 - y2 is V31() real ext-real Element of REAL
(1 - y2) * x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(1 - y2) * x2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
y2 * y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y2 * y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
((1 - y2) * x2) + (y2 * y1) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - y2) * x2) + (y2 * y1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
x2 `1 is V31() real ext-real Element of REAL
x2 . 1 is V31() real ext-real Element of REAL
(1 - y2) * (x2 `1) is V31() real ext-real Element of REAL
(1 - y2) * (x2 `2) is V31() real ext-real Element of REAL
|[((1 - y2) * (x2 `1)),((1 - y2) * (x2 `2))]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - y2) * x2) `2 is V31() real ext-real Element of REAL
((1 - y2) * x2) . 2 is V31() real ext-real Element of REAL
y1 `1 is V31() real ext-real Element of REAL
y1 . 1 is V31() real ext-real Element of REAL
y2 * (y1 `1) is V31() real ext-real Element of REAL
y2 * (y1 `2) is V31() real ext-real Element of REAL
|[(y2 * (y1 `1)),(y2 * (y1 `2))]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(y2 * y1) `2 is V31() real ext-real Element of REAL
(y2 * y1) . 2 is V31() real ext-real Element of REAL
((1 - y2) * x2) `1 is V31() real ext-real Element of REAL
((1 - y2) * x2) . 1 is V31() real ext-real Element of REAL
(y2 * y1) `1 is V31() real ext-real Element of REAL
(y2 * y1) . 1 is V31() real ext-real Element of REAL
(((1 - y2) * x2) `1) + ((y2 * y1) `1) is V31() real ext-real Element of REAL
(((1 - y2) * x2) `2) + ((y2 * y1) `2) is V31() real ext-real Element of REAL
|[((((1 - y2) * x2) `1) + ((y2 * y1) `1)),((((1 - y2) * x2) `2) + ((y2 * y1) `2))]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
((1 - y2) * (x2 `2)) + (y2 * (y1 `2)) is V31() real ext-real Element of REAL
(x2 `2) - (x1 `2) is V31() real ext-real Element of REAL
y2 * ((x2 `2) - (y1 `2)) is V31() real ext-real Element of REAL
(y1 `2) - (x2 `2) is V31() real ext-real Element of REAL
(y1 `2) - (x1 `2) is V31() real ext-real Element of REAL
(1 - y2) * ((y1 `2) - (x2 `2)) is V31() real ext-real Element of REAL
x1 is non empty Element of bool the carrier of (TOP-REAL 2)
W-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | x1 is non empty Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is non empty set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
lower_bound (proj1 | x1) is V31() real ext-real Element of REAL
(proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1) is non empty V202() V203() V204() Element of bool REAL
lower_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(W-bound x1) - 1 is V31() real ext-real Element of REAL
x2 `2 is V31() real ext-real Element of REAL
x2 . 2 is V31() real ext-real Element of REAL
(x2 `2) - 1 is V31() real ext-real Element of REAL
|[((W-bound x1) - 1),((x2 `2) - 1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 `1 is V31() real ext-real Element of REAL
y1 . 1 is V31() real ext-real Element of REAL
(W-bound x1) - 0 is V31() real ext-real Element of REAL
(x2 `2) - 0 is V31() real ext-real Element of REAL
x1 is non empty Element of bool the carrier of (TOP-REAL 2)
E-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | x1 is non empty Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is non empty set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
upper_bound (proj1 | x1) is V31() real ext-real Element of REAL
(proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1) is non empty V202() V203() V204() Element of bool REAL
upper_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(E-bound x1) + 1 is V31() real ext-real Element of REAL
x2 `2 is V31() real ext-real Element of REAL
x2 . 2 is V31() real ext-real Element of REAL
(x2 `2) - 1 is V31() real ext-real Element of REAL
|[((E-bound x1) + 1),((x2 `2) - 1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 `1 is V31() real ext-real Element of REAL
y1 . 1 is V31() real ext-real Element of REAL
(E-bound x1) + 0 is V31() real ext-real Element of REAL
(x2 `2) - 0 is V31() real ext-real Element of REAL
x1 is non empty Element of bool the carrier of (TOP-REAL 2)
N-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | x1 is non empty Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is non empty set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
upper_bound (proj2 | x1) is V31() real ext-real Element of REAL
(proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1) is non empty V202() V203() V204() Element of bool REAL
upper_bound ((proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 `1 is V31() real ext-real Element of REAL
x2 . 1 is V31() real ext-real Element of REAL
(x2 `1) - 1 is V31() real ext-real Element of REAL
(N-bound x1) + 1 is V31() real ext-real Element of REAL
|[((x2 `1) - 1),((N-bound x1) + 1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 `2 is V31() real ext-real Element of REAL
y1 . 2 is V31() real ext-real Element of REAL
(N-bound x1) + 0 is V31() real ext-real Element of REAL
(x2 `1) - 0 is V31() real ext-real Element of REAL
x1 is non empty Element of bool the carrier of (TOP-REAL 2)
S-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | x1 is non empty Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is non empty set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
lower_bound (proj2 | x1) is V31() real ext-real Element of REAL
(proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1) is non empty V202() V203() V204() Element of bool REAL
lower_bound ((proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 `1 is V31() real ext-real Element of REAL
x2 . 1 is V31() real ext-real Element of REAL
(x2 `1) - 1 is V31() real ext-real Element of REAL
(S-bound x1) - 1 is V31() real ext-real Element of REAL
|[((x2 `1) - 1),((S-bound x1) - 1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 `2 is V31() real ext-real Element of REAL
y1 . 2 is V31() real ext-real Element of REAL
(S-bound x1) - 0 is V31() real ext-real Element of REAL
(x2 `1) - 0 is V31() real ext-real Element of REAL
x1 is Element of bool the carrier of (TOP-REAL 2)
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 `2 is V31() real ext-real Element of REAL
x2 . 2 is V31() real ext-real Element of REAL
y1 `2 is V31() real ext-real Element of REAL
y1 . 2 is V31() real ext-real Element of REAL
x1 is Element of bool the carrier of (TOP-REAL 2)
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 `1 is V31() real ext-real Element of REAL
x2 . 1 is V31() real ext-real Element of REAL
y1 `1 is V31() real ext-real Element of REAL
y1 . 1 is V31() real ext-real Element of REAL
x1 is Element of bool the carrier of (TOP-REAL 2)
x1 is Element of bool the carrier of (TOP-REAL 2)
x1 is Element of bool the carrier of (TOP-REAL 2)
x1 is Element of bool the carrier of (TOP-REAL 2)
the non empty connected convex Element of bool the carrier of (TOP-REAL 2) is non empty connected convex Element of bool the carrier of (TOP-REAL 2)
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg (x1,x2) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * x1) + (b₁ * x2)) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[1,0]|)) is non empty Element of bool the carrier of (TOP-REAL 2)
(((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[0,0]|)) is non empty Element of bool the carrier of (TOP-REAL 2)
x1 is Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | R^2-unit_square is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | R^2-unit_square) is non empty set
(TOP-REAL 2) | x1 is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | x1) is set
[: the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | x1):] is set
bool [: the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | x1):] is non empty set
x2 is Relation-like the carrier of ((TOP-REAL 2) | R^2-unit_square) -defined the carrier of ((TOP-REAL 2) | x1) -valued Function-like quasi_total Element of bool [: the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | x1):]
x1 is Element of bool the carrier of (TOP-REAL 2)
NE-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
E-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | x1 is Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
upper_bound (proj1 | x1) is V31() real ext-real Element of REAL
(proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1) is V202() V203() V204() Element of bool REAL
upper_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
N-bound x1 is V31() real ext-real Element of REAL
proj2 | x1 is Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
upper_bound (proj2 | x1) is V31() real ext-real Element of REAL
(proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1) is V202() V203() V204() Element of bool REAL
upper_bound ((proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
|[(E-bound x1),(N-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
SE-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
S-bound x1 is V31() real ext-real Element of REAL
lower_bound (proj2 | x1) is V31() real ext-real Element of REAL
lower_bound ((proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
|[(E-bound x1),(S-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg ((NE-corner x1),(SE-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (NE-corner x1)) + (b₁ * (SE-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
SpStSeq x1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (SpStSeq x1) is boundary compact bounded Element of bool the carrier of (TOP-REAL 2)
NW-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
W-bound x1 is V31() real ext-real Element of REAL
lower_bound (proj1 | x1) is V31() real ext-real Element of REAL
lower_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
|[(W-bound x1),(N-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner x1),(NE-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (NW-corner x1)) + (b₁ * (NE-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
SW-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|[(W-bound x1),(S-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner x1),(SW-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (SE-corner x1)) + (b₁ * (SW-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg ((SW-corner x1),(NW-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (SW-corner x1)) + (b₁ * (NW-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg ((SE-corner x1),(SW-corner x1))) \/ (LSeg ((SW-corner x1),(NW-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
((LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1)))) \/ ((LSeg ((SE-corner x1),(SW-corner x1))) \/ (LSeg ((SW-corner x1),(NW-corner x1)))) is non empty Element of bool the carrier of (TOP-REAL 2)
x1 is Element of bool the carrier of (TOP-REAL 2)
SW-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
W-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | x1 is Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
lower_bound (proj1 | x1) is V31() real ext-real Element of REAL
(proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1) is V202() V203() V204() Element of bool REAL
lower_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
S-bound x1 is V31() real ext-real Element of REAL
proj2 | x1 is Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
lower_bound (proj2 | x1) is V31() real ext-real Element of REAL
(proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1) is V202() V203() V204() Element of bool REAL
lower_bound ((proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
|[(W-bound x1),(S-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
SE-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
E-bound x1 is V31() real ext-real Element of REAL
upper_bound (proj1 | x1) is V31() real ext-real Element of REAL
upper_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
|[(E-bound x1),(S-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner x1),(SE-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (SW-corner x1)) + (b₁ * (SE-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
SpStSeq x1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (SpStSeq x1) is boundary compact bounded Element of bool the carrier of (TOP-REAL 2)
NW-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
N-bound x1 is V31() real ext-real Element of REAL
upper_bound (proj2 | x1) is V31() real ext-real Element of REAL
upper_bound ((proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
|[(W-bound x1),(N-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
NE-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|[(E-bound x1),(N-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner x1),(NE-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (NW-corner x1)) + (b₁ * (NE-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg ((NE-corner x1),(SE-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (NE-corner x1)) + (b₁ * (SE-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
LSeg ((SE-corner x1),(SW-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (SE-corner x1)) + (b₁ * (SW-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
((LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1)))) \/ (LSeg ((SE-corner x1),(SW-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
LSeg ((SW-corner x1),(NW-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (SW-corner x1)) + (b₁ * (NW-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(((LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1)))) \/ (LSeg ((SE-corner x1),(SW-corner x1)))) \/ (LSeg ((SW-corner x1),(NW-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
(LSeg ((SE-corner x1),(SW-corner x1))) \/ (LSeg ((SW-corner x1),(NW-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
((LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1)))) \/ ((LSeg ((SE-corner x1),(SW-corner x1))) \/ (LSeg ((SW-corner x1),(NW-corner x1)))) is non empty Element of bool the carrier of (TOP-REAL 2)
((LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1)))) \/ (LSeg ((SW-corner x1),(SE-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
x1 is Element of bool the carrier of (TOP-REAL 2)
SW-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
W-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | x1 is Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
lower_bound (proj1 | x1) is V31() real ext-real Element of REAL
(proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1) is V202() V203() V204() Element of bool REAL
lower_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
S-bound x1 is V31() real ext-real Element of REAL
proj2 | x1 is Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
lower_bound (proj2 | x1) is V31() real ext-real Element of REAL
(proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1) is V202() V203() V204() Element of bool REAL
lower_bound ((proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
|[(W-bound x1),(S-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
NW-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
N-bound x1 is V31() real ext-real Element of REAL
upper_bound (proj2 | x1) is V31() real ext-real Element of REAL
upper_bound ((proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
|[(W-bound x1),(N-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner x1),(NW-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (SW-corner x1)) + (b₁ * (NW-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
SpStSeq x1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (SpStSeq x1) is boundary compact bounded Element of bool the carrier of (TOP-REAL 2)
NE-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
E-bound x1 is V31() real ext-real Element of REAL
upper_bound (proj1 | x1) is V31() real ext-real Element of REAL
upper_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
|[(E-bound x1),(N-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner x1),(NE-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (NW-corner x1)) + (b₁ * (NE-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
SE-corner x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|[(E-bound x1),(S-bound x1)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg ((NE-corner x1),(SE-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (NE-corner x1)) + (b₁ * (SE-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
LSeg ((SE-corner x1),(SW-corner x1)) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b₁) * (SE-corner x1)) + (b₁ * (SW-corner x1))) where b₁ is V31() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
((LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1)))) \/ (LSeg ((SE-corner x1),(SW-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
(((LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1)))) \/ (LSeg ((SE-corner x1),(SW-corner x1)))) \/ (LSeg ((SW-corner x1),(NW-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
(LSeg ((SE-corner x1),(SW-corner x1))) \/ (LSeg ((SW-corner x1),(NW-corner x1))) is non empty Element of bool the carrier of (TOP-REAL 2)
((LSeg ((NW-corner x1),(NE-corner x1))) \/ (LSeg ((NE-corner x1),(SE-corner x1)))) \/ ((LSeg ((SE-corner x1),(SW-corner x1))) \/ (LSeg ((SW-corner x1),(NW-corner x1)))) is non empty Element of bool the carrier of (TOP-REAL 2)
x1 is Element of bool the carrier of (TOP-REAL 2)
W-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | x1 is Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
lower_bound (proj1 | x1) is V31() real ext-real Element of REAL
(proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1) is V202() V203() V204() Element of bool REAL
lower_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
{ b₁ where b₁ is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2) : not W-bound x1 <= b₁ `1 } is set
y1 is set
y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y2 `1 is V31() real ext-real Element of REAL
y2 . 1 is V31() real ext-real Element of REAL
(W-bound x1) - 1 is V31() real ext-real Element of REAL
|[((W-bound x1) - 1),0]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|[((W-bound x1) - 1),0]| `1 is V31() real ext-real Element of REAL
|[((W-bound x1) - 1),0]| . 1 is V31() real ext-real Element of REAL
(W-bound x1) - 0 is V31() real ext-real Element of REAL
y1 is Element of bool the carrier of (TOP-REAL 2)
b is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
O is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
LSeg (b,O) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b<sub>1</sub>) * b) + (b<sub>1</sub> * O)) where b<sub>1</sub> is V31() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
g is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
g `1 is V31() real ext-real Element of REAL
g . 1 is V31() real ext-real Element of REAL
g is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
g `1 is V31() real ext-real Element of REAL
g . 1 is V31() real ext-real Element of REAL
B is set
d is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
d `1 is V31() real ext-real Element of REAL
d . 1 is V31() real ext-real Element of REAL
O `1 is V31() real ext-real Element of REAL
O . 1 is V31() real ext-real Element of REAL
d is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
d `1 is V31() real ext-real Element of REAL
d . 1 is V31() real ext-real Element of REAL
b `1 is V31() real ext-real Element of REAL
b . 1 is V31() real ext-real Element of REAL
d is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
d `1 is V31() real ext-real Element of REAL
d . 1 is V31() real ext-real Element of REAL
b is non empty connected convex Element of bool the carrier of (TOP-REAL 2)
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `1 is V31() real ext-real Element of REAL
x1 . 1 is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 `1 is V31() real ext-real Element of REAL
x2 . 1 is V31() real ext-real Element of REAL
y1 is Element of the carrier of (Euclid 2)
y2 is V31() real ext-real set
Ball (y1,y2) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
(x1 `1) - y2 is V31() real ext-real Element of REAL
(x1 `1) + y2 is V31() real ext-real Element of REAL
a is Element of the carrier of (Euclid 2)
dist (y1,a) is V31() real ext-real Element of REAL
(Pitag_dist 2) . (y1,a) is set
[y1,a] is set
{y1,a} is non empty finite set
{y1} is non empty finite set
{{y1,a},{y1}} is non empty finite V40() set
(Pitag_dist 2) . [y1,a] is V31() real ext-real set
(x1 `1) - (x2 `1) is V31() real ext-real Element of REAL
((x1 `1) - (x2 `1)) ^2 is V31() real ext-real Element of REAL
((x1 `1) - (x2 `1)) * ((x1 `1) - (x2 `1)) is V31() real ext-real set
x1 `2 is V31() real ext-real Element of REAL
x1 . 2 is V31() real ext-real Element of REAL
x2 `2 is V31() real ext-real Element of REAL
x2 . 2 is V31() real ext-real Element of REAL
(x1 `2) - (x2 `2) is V31() real ext-real Element of REAL
((x1 `2) - (x2 `2)) ^2 is V31() real ext-real Element of REAL
((x1 `2) - (x2 `2)) * ((x1 `2) - (x2 `2)) is V31() real ext-real set
(((x1 `1) - (x2 `1)) ^2) + (((x1 `2) - (x2 `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((x1 `1) - (x2 `1)) ^2) + (((x1 `2) - (x2 `2)) ^2)) is V31() real ext-real Element of REAL
(((x1 `1) - (x2 `1)) ^2) + 0 is V31() real ext-real Element of REAL
y2 ^2 is V31() real ext-real set
y2 * y2 is V31() real ext-real set
sqrt (y2 ^2) is V31() real ext-real set
(((x1 `1) - (x2 `1)) ^2) + 0 is V31() real ext-real Element of REAL
(x2 `1) - (x1 `1) is V31() real ext-real Element of REAL
y2 ^2 is V31() real ext-real set
y2 * y2 is V31() real ext-real set
- ((x1 `1) - (x2 `1)) is V31() real ext-real Element of REAL
(- ((x1 `1) - (x2 `1))) ^2 is V31() real ext-real Element of REAL
(- ((x1 `1) - (x2 `1))) * (- ((x1 `1) - (x2 `1))) is V31() real ext-real set
sqrt (y2 ^2) is V31() real ext-real set
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `2 is V31() real ext-real Element of REAL
x1 . 2 is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 `2 is V31() real ext-real Element of REAL
x2 . 2 is V31() real ext-real Element of REAL
y1 is Element of the carrier of (Euclid 2)
y2 is V31() real ext-real set
Ball (y1,y2) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
(x1 `2) - y2 is V31() real ext-real Element of REAL
(x1 `2) + y2 is V31() real ext-real Element of REAL
a is Element of the carrier of (Euclid 2)
dist (y1,a) is V31() real ext-real Element of REAL
(Pitag_dist 2) . (y1,a) is set
[y1,a] is set
{y1,a} is non empty finite set
{y1} is non empty finite set
{{y1,a},{y1}} is non empty finite V40() set
(Pitag_dist 2) . [y1,a] is V31() real ext-real set
x1 `1 is V31() real ext-real Element of REAL
x1 . 1 is V31() real ext-real Element of REAL
x2 `1 is V31() real ext-real Element of REAL
x2 . 1 is V31() real ext-real Element of REAL
(x1 `1) - (x2 `1) is V31() real ext-real Element of REAL
((x1 `1) - (x2 `1)) ^2 is V31() real ext-real Element of REAL
((x1 `1) - (x2 `1)) * ((x1 `1) - (x2 `1)) is V31() real ext-real set
(x1 `2) - (x2 `2) is V31() real ext-real Element of REAL
((x1 `2) - (x2 `2)) ^2 is V31() real ext-real Element of REAL
((x1 `2) - (x2 `2)) * ((x1 `2) - (x2 `2)) is V31() real ext-real set
(((x1 `1) - (x2 `1)) ^2) + (((x1 `2) - (x2 `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((x1 `1) - (x2 `1)) ^2) + (((x1 `2) - (x2 `2)) ^2)) is V31() real ext-real Element of REAL
(((x1 `2) - (x2 `2)) ^2) + 0 is V31() real ext-real Element of REAL
y2 ^2 is V31() real ext-real set
y2 * y2 is V31() real ext-real set
sqrt (y2 ^2) is V31() real ext-real set
(((x1 `2) - (x2 `2)) ^2) + 0 is V31() real ext-real Element of REAL
(x2 `2) - (x1 `2) is V31() real ext-real Element of REAL
y2 ^2 is V31() real ext-real set
y2 * y2 is V31() real ext-real set
- ((x1 `2) - (x2 `2)) is V31() real ext-real Element of REAL
(- ((x1 `2) - (x2 `2))) ^2 is V31() real ext-real Element of REAL
(- ((x1 `2) - (x2 `2))) * (- ((x1 `2) - (x2 `2))) is V31() real ext-real set
sqrt (y2 ^2) is V31() real ext-real set
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `1 is V31() real ext-real Element of REAL
x1 . 1 is V31() real ext-real Element of REAL
x1 `2 is V31() real ext-real Element of REAL
x1 . 2 is V31() real ext-real Element of REAL
x2 is Element of the carrier of (Euclid 2)
y1 is V31() real ext-real set
y1 / (sqrt 2) is V31() real ext-real Element of REAL
(x1 `1) - (y1 / (sqrt 2)) is V31() real ext-real Element of REAL
(x1 `1) + (y1 / (sqrt 2)) is V31() real ext-real Element of REAL
].((x1 `1) - (y1 / (sqrt 2))),((x1 `1) + (y1 / (sqrt 2))).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
(x1 `2) - (y1 / (sqrt 2)) is V31() real ext-real Element of REAL
(x1 `2) + (y1 / (sqrt 2)) is V31() real ext-real Element of REAL
].((x1 `2) - (y1 / (sqrt 2))),((x1 `2) + (y1 / (sqrt 2))).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
(1,2) --> (].((x1 `1) - (y1 / (sqrt 2))),((x1 `1) + (y1 / (sqrt 2))).[,].((x1 `2) - (y1 / (sqrt 2))),((x1 `2) + (y1 / (sqrt 2))).[) is non empty Relation-like NAT -defined {1,2} -defined bool REAL -valued Function-like total quasi_total finite Element of bool [:{1,2},(bool REAL):]
[:{1,2},(bool REAL):] is non empty set
bool [:{1,2},(bool REAL):] is non empty set
product ((1,2) --> (].((x1 `1) - (y1 / (sqrt 2))),((x1 `1) + (y1 / (sqrt 2))).[,].((x1 `2) - (y1 / (sqrt 2))),((x1 `2) + (y1 / (sqrt 2))).[)) is set
Ball (x2,y1) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
O is set
{ b₁ where b₁ is V31() real ext-real Element of REAL : ( not b₁ <= (x1 `1) - (y1 / (sqrt 2)) & not (x1 `1) + (y1 / (sqrt 2)) <= b₁ ) } is set
((1,2) --> (].((x1 `1) - (y1 / (sqrt 2))),((x1 `1) + (y1 / (sqrt 2))).[,].((x1 `2) - (y1 / (sqrt 2))),((x1 `2) + (y1 / (sqrt 2))).[)) . 2 is set
{ b₁ where b₁ is V31() real ext-real Element of REAL : ( not b₁ <= (x1 `2) - (y1 / (sqrt 2)) & not (x1 `2) + (y1 / (sqrt 2)) <= b₁ ) } is set
((1,2) --> (].((x1 `1) - (y1 / (sqrt 2))),((x1 `1) + (y1 / (sqrt 2))).[,].((x1 `2) - (y1 / (sqrt 2))),((x1 `2) + (y1 / (sqrt 2))).[)) . 1 is set
dom ((1,2) --> (].((x1 `1) - (y1 / (sqrt 2))),((x1 `1) + (y1 / (sqrt 2))).[,].((x1 `2) - (y1 / (sqrt 2))),((x1 `2) + (y1 / (sqrt 2))).[)) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool {1,2}
bool {1,2} is non empty finite V40() set
g is Relation-like Function-like set
dom g is set
g . 1 is set
g is V31() real ext-real Element of REAL
g - (x1 `1) is V31() real ext-real Element of REAL
(g - (x1 `1)) ^2 is V31() real ext-real Element of REAL
(g - (x1 `1)) * (g - (x1 `1)) is V31() real ext-real set
g . 2 is set
B is V31() real ext-real Element of REAL
B - (x1 `2) is V31() real ext-real Element of REAL
abs (B - (x1 `2)) is V31() real ext-real Element of REAL
(y1 / (sqrt 2)) ^2 is V31() real ext-real Element of REAL
(y1 / (sqrt 2)) * (y1 / (sqrt 2)) is V31() real ext-real set
(abs (B - (x1 `2))) ^2 is V31() real ext-real Element of REAL
(abs (B - (x1 `2))) * (abs (B - (x1 `2))) is V31() real ext-real set
y1 ^2 is V31() real ext-real set
y1 * y1 is V31() real ext-real set
(sqrt 2) ^2 is V31() real ext-real Element of REAL
(sqrt 2) * (sqrt 2) is V31() real ext-real set
(y1 ^2) / ((sqrt 2) ^2) is V31() real ext-real Element of REAL
(y1 ^2) / 2 is V31() real ext-real Element of REAL
(B - (x1 `2)) ^2 is V31() real ext-real Element of REAL
(B - (x1 `2)) * (B - (x1 `2)) is V31() real ext-real set
(x1 `1) - ((x1 `1) - (y1 / (sqrt 2))) is V31() real ext-real Element of REAL
(x1 `1) - ((x1 `1) + (y1 / (sqrt 2))) is V31() real ext-real Element of REAL
(y1 / (sqrt 2)) + (y1 / (sqrt 2)) is V31() real ext-real Element of REAL
- (y1 / (sqrt 2)) is V31() real ext-real Element of REAL
(- (y1 / (sqrt 2))) + (y1 / (sqrt 2)) is V31() real ext-real Element of REAL
d is set
g . d is set
<*(g . 1),(g . 2)*> is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like set
<*(g . 1),(g . 2)*> . d is set
abs (g - (x1 `1)) is V31() real ext-real Element of REAL
(abs (g - (x1 `1))) ^2 is V31() real ext-real Element of REAL
(abs (g - (x1 `1))) * (abs (g - (x1 `1))) is V31() real ext-real set
((y1 ^2) / 2) + ((y1 ^2) / 2) is V31() real ext-real Element of REAL
((g - (x1 `1)) ^2) + ((B - (x1 `2)) ^2) is V31() real ext-real Element of REAL
sqrt (y1 ^2) is V31() real ext-real set
sqrt (((g - (x1 `1)) ^2) + ((B - (x1 `2)) ^2)) is V31() real ext-real Element of REAL
dom <*(g . 1),(g . 2)*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
|[g,B]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
d is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
r is Element of the carrier of (Euclid 2)
dist (r,x2) is V31() real ext-real Element of REAL
(Pitag_dist 2) . (r,x2) is set
[r,x2] is set
{r,x2} is non empty finite set
{r} is non empty finite set
{{r,x2},{r}} is non empty finite V40() set
(Pitag_dist 2) . [r,x2] is V31() real ext-real set
d `1 is V31() real ext-real Element of REAL
d . 1 is V31() real ext-real Element of REAL
(d `1) - (x1 `1) is V31() real ext-real Element of REAL
((d `1) - (x1 `1)) ^2 is V31() real ext-real Element of REAL
((d `1) - (x1 `1)) * ((d `1) - (x1 `1)) is V31() real ext-real set
d `2 is V31() real ext-real Element of REAL
d . 2 is V31() real ext-real Element of REAL
(d `2) - (x1 `2) is V31() real ext-real Element of REAL
((d `2) - (x1 `2)) ^2 is V31() real ext-real Element of REAL
((d `2) - (x1 `2)) * ((d `2) - (x1 `2)) is V31() real ext-real set
(((d `1) - (x1 `1)) ^2) + (((d `2) - (x1 `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((d `1) - (x1 `1)) ^2) + (((d `2) - (x1 `2)) ^2)) is V31() real ext-real Element of REAL
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `1 is V31() real ext-real Element of REAL
x1 . 1 is V31() real ext-real Element of REAL
x1 `2 is V31() real ext-real Element of REAL
x1 . 2 is V31() real ext-real Element of REAL
x2 is Element of the carrier of (Euclid 2)
y1 is V31() real ext-real set
Ball (x2,y1) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
(x1 `1) - y1 is V31() real ext-real Element of REAL
(x1 `1) + y1 is V31() real ext-real Element of REAL
].((x1 `1) - y1),((x1 `1) + y1).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
(x1 `2) - y1 is V31() real ext-real Element of REAL
(x1 `2) + y1 is V31() real ext-real Element of REAL
].((x1 `2) - y1),((x1 `2) + y1).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
(1,2) --> (].((x1 `1) - y1),((x1 `1) + y1).[,].((x1 `2) - y1),((x1 `2) + y1).[) is non empty Relation-like NAT -defined {1,2} -defined bool REAL -valued Function-like total quasi_total finite Element of bool [:{1,2},(bool REAL):]
[:{1,2},(bool REAL):] is non empty set
bool [:{1,2},(bool REAL):] is non empty set
product ((1,2) --> (].((x1 `1) - y1),((x1 `1) + y1).[,].((x1 `2) - y1),((x1 `2) + y1).[)) is set
O is set
g is Element of the carrier of (Euclid 2)
g is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
dom ((1,2) --> (].((x1 `1) - y1),((x1 `1) + y1).[,].((x1 `2) - y1),((x1 `2) + y1).[)) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool {1,2}
bool {1,2} is non empty finite V40() set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
d is set
B . d is set
((1,2) --> (].((x1 `1) - y1),((x1 `1) + y1).[,].((x1 `2) - y1),((x1 `2) + y1).[)) . d is set
((1,2) --> (].((x1 `1) - y1),((x1 `1) + y1).[,].((x1 `2) - y1),((x1 `2) + y1).[)) . 1 is set
g `1 is V31() real ext-real Element of REAL
g . 1 is V31() real ext-real Element of REAL
((1,2) --> (].((x1 `1) - y1),((x1 `1) + y1).[,].((x1 `2) - y1),((x1 `2) + y1).[)) . 2 is set
g `2 is V31() real ext-real Element of REAL
g . 2 is V31() real ext-real Element of REAL
[:(Seg 2),REAL:] is non empty complex-yielding V193() V194() set
bool [:(Seg 2),REAL:] is non empty set
dom B is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `1 is V31() real ext-real Element of REAL
x1 . 1 is V31() real ext-real Element of REAL
x2 is Element of the carrier of (Euclid 2)
y1 is Element of bool the carrier of (TOP-REAL 2)
proj1 .: y1 is V202() V203() V204() Element of bool REAL
y2 is V31() real ext-real set
Ball (x2,y2) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
(x1 `1) - y2 is V31() real ext-real Element of REAL
(x1 `1) + y2 is V31() real ext-real Element of REAL
].((x1 `1) - y2),((x1 `1) + y2).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
a is set
b is set
proj1 . b is V31() real ext-real Element of REAL
g is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
g `1 is V31() real ext-real Element of REAL
g . 1 is V31() real ext-real Element of REAL
O is V31() real ext-real Element of REAL
a is set
b is V31() real ext-real Element of REAL
x1 `2 is V31() real ext-real Element of REAL
x1 . 2 is V31() real ext-real Element of REAL
|[b,(x1 `2)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
O is Element of the carrier of (Euclid 2)
dist (O,x2) is V31() real ext-real Element of REAL
(Pitag_dist 2) . (O,x2) is set
[O,x2] is set
{O,x2} is non empty finite set
{O} is non empty finite set
{{O,x2},{O}} is non empty finite V40() set
(Pitag_dist 2) . [O,x2] is V31() real ext-real set
|[b,(x1 `2)]| `1 is V31() real ext-real Element of REAL
|[b,(x1 `2)]| . 1 is V31() real ext-real Element of REAL
(|[b,(x1 `2)]| `1) - (x1 `1) is V31() real ext-real Element of REAL
((|[b,(x1 `2)]| `1) - (x1 `1)) ^2 is V31() real ext-real Element of REAL
((|[b,(x1 `2)]| `1) - (x1 `1)) * ((|[b,(x1 `2)]| `1) - (x1 `1)) is V31() real ext-real set
|[b,(x1 `2)]| `2 is V31() real ext-real Element of REAL
|[b,(x1 `2)]| . 2 is V31() real ext-real Element of REAL
(|[b,(x1 `2)]| `2) - (x1 `2) is V31() real ext-real Element of REAL
((|[b,(x1 `2)]| `2) - (x1 `2)) ^2 is V31() real ext-real Element of REAL
((|[b,(x1 `2)]| `2) - (x1 `2)) * ((|[b,(x1 `2)]| `2) - (x1 `2)) is V31() real ext-real set
(((|[b,(x1 `2)]| `1) - (x1 `1)) ^2) + (((|[b,(x1 `2)]| `2) - (x1 `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((|[b,(x1 `2)]| `1) - (x1 `1)) ^2) + (((|[b,(x1 `2)]| `2) - (x1 `2)) ^2)) is V31() real ext-real Element of REAL
b - (x1 `1) is V31() real ext-real Element of REAL
(b - (x1 `1)) ^2 is V31() real ext-real Element of REAL
(b - (x1 `1)) * (b - (x1 `1)) is V31() real ext-real set
((b - (x1 `1)) ^2) + (((|[b,(x1 `2)]| `2) - (x1 `2)) ^2) is V31() real ext-real Element of REAL
sqrt (((b - (x1 `1)) ^2) + (((|[b,(x1 `2)]| `2) - (x1 `2)) ^2)) is V31() real ext-real Element of REAL
(x1 `2) - (x1 `2) is V31() real ext-real Element of REAL
((x1 `2) - (x1 `2)) ^2 is V31() real ext-real Element of REAL
((x1 `2) - (x1 `2)) * ((x1 `2) - (x1 `2)) is V31() real ext-real set
((b - (x1 `1)) ^2) + (((x1 `2) - (x1 `2)) ^2) is V31() real ext-real Element of REAL
sqrt (((b - (x1 `1)) ^2) + (((x1 `2) - (x1 `2)) ^2)) is V31() real ext-real Element of REAL
((b - (x1 `1)) ^2) + 0 is V31() real ext-real Element of REAL
sqrt (((b - (x1 `1)) ^2) + 0) is V31() real ext-real Element of REAL
((x1 `1) + y2) - (x1 `1) is V31() real ext-real Element of REAL
b + y2 is V31() real ext-real Element of REAL
((x1 `1) - y2) + y2 is V31() real ext-real Element of REAL
y2 + b is V31() real ext-real Element of REAL
(y2 + b) - b is V31() real ext-real Element of REAL
(x1 `1) - b is V31() real ext-real Element of REAL
sqrt ((b - (x1 `1)) ^2) is V31() real ext-real Element of REAL
- (b - (x1 `1)) is V31() real ext-real Element of REAL
(- (b - (x1 `1))) ^2 is V31() real ext-real Element of REAL
(- (b - (x1 `1))) * (- (b - (x1 `1))) is V31() real ext-real set
sqrt ((- (b - (x1 `1))) ^2) is V31() real ext-real Element of REAL
proj1 . |[b,(x1 `2)]| is V31() real ext-real Element of REAL
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `2 is V31() real ext-real Element of REAL
x1 . 2 is V31() real ext-real Element of REAL
x2 is Element of the carrier of (Euclid 2)
y1 is Element of bool the carrier of (TOP-REAL 2)
proj2 .: y1 is V202() V203() V204() Element of bool REAL
y2 is V31() real ext-real set
Ball (x2,y2) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
(x1 `2) - y2 is V31() real ext-real Element of REAL
(x1 `2) + y2 is V31() real ext-real Element of REAL
].((x1 `2) - y2),((x1 `2) + y2).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
a is set
b is set
proj2 . b is V31() real ext-real Element of REAL
g is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
g `2 is V31() real ext-real Element of REAL
g . 2 is V31() real ext-real Element of REAL
O is V31() real ext-real Element of REAL
a is set
x1 `1 is V31() real ext-real Element of REAL
x1 . 1 is V31() real ext-real Element of REAL
b is V31() real ext-real Element of REAL
|[(x1 `1),b]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
O is Element of the carrier of (Euclid 2)
dist (O,x2) is V31() real ext-real Element of REAL
(Pitag_dist 2) . (O,x2) is set
[O,x2] is set
{O,x2} is non empty finite set
{O} is non empty finite set
{{O,x2},{O}} is non empty finite V40() set
(Pitag_dist 2) . [O,x2] is V31() real ext-real set
|[(x1 `1),b]| `1 is V31() real ext-real Element of REAL
|[(x1 `1),b]| . 1 is V31() real ext-real Element of REAL
(|[(x1 `1),b]| `1) - (x1 `1) is V31() real ext-real Element of REAL
((|[(x1 `1),b]| `1) - (x1 `1)) ^2 is V31() real ext-real Element of REAL
((|[(x1 `1),b]| `1) - (x1 `1)) * ((|[(x1 `1),b]| `1) - (x1 `1)) is V31() real ext-real set
|[(x1 `1),b]| `2 is V31() real ext-real Element of REAL
|[(x1 `1),b]| . 2 is V31() real ext-real Element of REAL
(|[(x1 `1),b]| `2) - (x1 `2) is V31() real ext-real Element of REAL
((|[(x1 `1),b]| `2) - (x1 `2)) ^2 is V31() real ext-real Element of REAL
((|[(x1 `1),b]| `2) - (x1 `2)) * ((|[(x1 `1),b]| `2) - (x1 `2)) is V31() real ext-real set
(((|[(x1 `1),b]| `1) - (x1 `1)) ^2) + (((|[(x1 `1),b]| `2) - (x1 `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((|[(x1 `1),b]| `1) - (x1 `1)) ^2) + (((|[(x1 `1),b]| `2) - (x1 `2)) ^2)) is V31() real ext-real Element of REAL
(x1 `1) - (x1 `1) is V31() real ext-real Element of REAL
((x1 `1) - (x1 `1)) ^2 is V31() real ext-real Element of REAL
((x1 `1) - (x1 `1)) * ((x1 `1) - (x1 `1)) is V31() real ext-real set
(((x1 `1) - (x1 `1)) ^2) + (((|[(x1 `1),b]| `2) - (x1 `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((x1 `1) - (x1 `1)) ^2) + (((|[(x1 `1),b]| `2) - (x1 `2)) ^2)) is V31() real ext-real Element of REAL
b - (x1 `2) is V31() real ext-real Element of REAL
(b - (x1 `2)) ^2 is V31() real ext-real Element of REAL
(b - (x1 `2)) * (b - (x1 `2)) is V31() real ext-real set
0 + ((b - (x1 `2)) ^2) is V31() real ext-real Element of REAL
sqrt (0 + ((b - (x1 `2)) ^2)) is V31() real ext-real Element of REAL
((x1 `2) + y2) - (x1 `2) is V31() real ext-real Element of REAL
b + y2 is V31() real ext-real Element of REAL
((x1 `2) - y2) + y2 is V31() real ext-real Element of REAL
y2 + b is V31() real ext-real Element of REAL
(y2 + b) - b is V31() real ext-real Element of REAL
(x1 `2) - b is V31() real ext-real Element of REAL
sqrt ((b - (x1 `2)) ^2) is V31() real ext-real Element of REAL
- (b - (x1 `2)) is V31() real ext-real Element of REAL
(- (b - (x1 `2))) ^2 is V31() real ext-real Element of REAL
(- (b - (x1 `2))) * (- (b - (x1 `2))) is V31() real ext-real set
sqrt ((- (b - (x1 `2))) ^2) is V31() real ext-real Element of REAL
proj2 . |[(x1 `1),b]| is V31() real ext-real Element of REAL
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `1 is V31() real ext-real Element of REAL
x1 . 1 is V31() real ext-real Element of REAL
x2 is Element of the carrier of (Euclid 2)
y1 is non empty Element of bool the carrier of (TOP-REAL 2)
W-bound y1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | y1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | y1 is non empty Relation-like the carrier of ((TOP-REAL 2) | y1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | y1),REAL:]
the carrier of ((TOP-REAL 2) | y1) is non empty set
[: the carrier of ((TOP-REAL 2) | y1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | y1),REAL:] is non empty set
lower_bound (proj1 | y1) is V31() real ext-real Element of REAL
(proj1 | y1) .: the carrier of ((TOP-REAL 2) | y1) is non empty V202() V203() V204() Element of bool REAL
lower_bound ((proj1 | y1) .: the carrier of ((TOP-REAL 2) | y1)) is V31() real ext-real Element of REAL
y2 is V31() real ext-real set
Ball (x2,y2) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
(x1 `1) - y2 is V31() real ext-real Element of REAL
(x1 `1) + y2 is V31() real ext-real Element of REAL
(x1 `1) + 0 is V31() real ext-real Element of REAL
(x1 `1) - 0 is V31() real ext-real Element of REAL
].((x1 `1) - y2),((x1 `1) + y2).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
lower_bound ].((x1 `1) - y2),((x1 `1) + y2).[ is V31() real ext-real Element of REAL
proj1 .: y1 is non empty V202() V203() V204() Element of bool REAL
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `1 is V31() real ext-real Element of REAL
x1 . 1 is V31() real ext-real Element of REAL
x2 is Element of the carrier of (Euclid 2)
y1 is non empty Element of bool the carrier of (TOP-REAL 2)
E-bound y1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | y1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | y1 is non empty Relation-like the carrier of ((TOP-REAL 2) | y1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | y1),REAL:]
the carrier of ((TOP-REAL 2) | y1) is non empty set
[: the carrier of ((TOP-REAL 2) | y1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | y1),REAL:] is non empty set
upper_bound (proj1 | y1) is V31() real ext-real Element of REAL
(proj1 | y1) .: the carrier of ((TOP-REAL 2) | y1) is non empty V202() V203() V204() Element of bool REAL
upper_bound ((proj1 | y1) .: the carrier of ((TOP-REAL 2) | y1)) is V31() real ext-real Element of REAL
y2 is V31() real ext-real set
Ball (x2,y2) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
(x1 `1) + y2 is V31() real ext-real Element of REAL
(x1 `1) + 0 is V31() real ext-real Element of REAL
(x1 `1) - 0 is V31() real ext-real Element of REAL
(x1 `1) - y2 is V31() real ext-real Element of REAL
].((x1 `1) - y2),((x1 `1) + y2).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
upper_bound ].((x1 `1) - y2),((x1 `1) + y2).[ is V31() real ext-real Element of REAL
proj1 .: y1 is non empty V202() V203() V204() Element of bool REAL
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `2 is V31() real ext-real Element of REAL
x1 . 2 is V31() real ext-real Element of REAL
x2 is Element of the carrier of (Euclid 2)
y1 is non empty Element of bool the carrier of (TOP-REAL 2)
S-bound y1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | y1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | y1 is non empty Relation-like the carrier of ((TOP-REAL 2) | y1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | y1),REAL:]
the carrier of ((TOP-REAL 2) | y1) is non empty set
[: the carrier of ((TOP-REAL 2) | y1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | y1),REAL:] is non empty set
lower_bound (proj2 | y1) is V31() real ext-real Element of REAL
(proj2 | y1) .: the carrier of ((TOP-REAL 2) | y1) is non empty V202() V203() V204() Element of bool REAL
lower_bound ((proj2 | y1) .: the carrier of ((TOP-REAL 2) | y1)) is V31() real ext-real Element of REAL
y2 is V31() real ext-real set
Ball (x2,y2) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
(x1 `2) - y2 is V31() real ext-real Element of REAL
(x1 `2) + y2 is V31() real ext-real Element of REAL
(x1 `2) + 0 is V31() real ext-real Element of REAL
(x1 `2) - 0 is V31() real ext-real Element of REAL
].((x1 `2) - y2),((x1 `2) + y2).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
lower_bound ].((x1 `2) - y2),((x1 `2) + y2).[ is V31() real ext-real Element of REAL
proj2 .: y1 is non empty V202() V203() V204() Element of bool REAL
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `2 is V31() real ext-real Element of REAL
x1 . 2 is V31() real ext-real Element of REAL
x2 is Element of the carrier of (Euclid 2)
y1 is non empty Element of bool the carrier of (TOP-REAL 2)
N-bound y1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | y1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | y1 is non empty Relation-like the carrier of ((TOP-REAL 2) | y1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | y1),REAL:]
the carrier of ((TOP-REAL 2) | y1) is non empty set
[: the carrier of ((TOP-REAL 2) | y1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | y1),REAL:] is non empty set
upper_bound (proj2 | y1) is V31() real ext-real Element of REAL
(proj2 | y1) .: the carrier of ((TOP-REAL 2) | y1) is non empty V202() V203() V204() Element of bool REAL
upper_bound ((proj2 | y1) .: the carrier of ((TOP-REAL 2) | y1)) is V31() real ext-real Element of REAL
y2 is V31() real ext-real set
Ball (x2,y2) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
(x1 `2) + y2 is V31() real ext-real Element of REAL
(x1 `2) + 0 is V31() real ext-real Element of REAL
(x1 `2) - 0 is V31() real ext-real Element of REAL
(x1 `2) - y2 is V31() real ext-real Element of REAL
].((x1 `2) - y2),((x1 `2) + y2).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
upper_bound ].((x1 `2) - y2),((x1 `2) + y2).[ is V31() real ext-real Element of REAL
proj2 .: y1 is non empty V202() V203() V204() Element of bool REAL
x1 is Element of the carrier of (Euclid 2)
x2 is non empty Element of bool the carrier of (TOP-REAL 2)
y1 is V31() real ext-real set
Ball (x1,y1) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y2 `2 is V31() real ext-real Element of REAL
y2 . 2 is V31() real ext-real Element of REAL
y2 `1 is V31() real ext-real Element of REAL
y2 . 1 is V31() real ext-real Element of REAL
y1 / 2 is V31() real ext-real Element of REAL
(y2 `2) - (y1 / 2) is V31() real ext-real Element of REAL
|[(y2 `1),((y2 `2) - (y1 / 2))]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
a is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
a `2 is V31() real ext-real Element of REAL
a . 2 is V31() real ext-real Element of REAL
b is Element of the carrier of (Euclid 2)
dist (x1,b) is V31() real ext-real Element of REAL
(Pitag_dist 2) . (x1,b) is set
[x1,b] is set
{x1,b} is non empty finite set
{x1} is non empty finite set
{{x1,b},{x1}} is non empty finite V40() set
(Pitag_dist 2) . [x1,b] is V31() real ext-real set
a `1 is V31() real ext-real Element of REAL
a . 1 is V31() real ext-real Element of REAL
(y2 `1) - (a `1) is V31() real ext-real Element of REAL
((y2 `1) - (a `1)) ^2 is V31() real ext-real Element of REAL
((y2 `1) - (a `1)) * ((y2 `1) - (a `1)) is V31() real ext-real set
(y2 `2) - (a `2) is V31() real ext-real Element of REAL
((y2 `2) - (a `2)) ^2 is V31() real ext-real Element of REAL
((y2 `2) - (a `2)) * ((y2 `2) - (a `2)) is V31() real ext-real set
(((y2 `1) - (a `1)) ^2) + (((y2 `2) - (a `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((y2 `1) - (a `1)) ^2) + (((y2 `2) - (a `2)) ^2)) is V31() real ext-real Element of REAL
(y2 `1) - (y2 `1) is V31() real ext-real Element of REAL
((y2 `1) - (y2 `1)) ^2 is V31() real ext-real Element of REAL
((y2 `1) - (y2 `1)) * ((y2 `1) - (y2 `1)) is V31() real ext-real set
(((y2 `1) - (y2 `1)) ^2) + (((y2 `2) - (a `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((y2 `1) - (y2 `1)) ^2) + (((y2 `2) - (a `2)) ^2)) is V31() real ext-real Element of REAL
(y2 `2) - ((y2 `2) - (y1 / 2)) is V31() real ext-real Element of REAL
((y2 `2) - ((y2 `2) - (y1 / 2))) ^2 is V31() real ext-real Element of REAL
((y2 `2) - ((y2 `2) - (y1 / 2))) * ((y2 `2) - ((y2 `2) - (y1 / 2))) is V31() real ext-real set
0 + (((y2 `2) - ((y2 `2) - (y1 / 2))) ^2) is V31() real ext-real Element of REAL
sqrt (0 + (((y2 `2) - ((y2 `2) - (y1 / 2))) ^2)) is V31() real ext-real Element of REAL
(y2 `2) - 0 is V31() real ext-real Element of REAL
x1 is Element of the carrier of (Euclid 2)
x2 is non empty Element of bool the carrier of (TOP-REAL 2)
y1 is V31() real ext-real set
Ball (x1,y1) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y2 `1 is V31() real ext-real Element of REAL
y2 . 1 is V31() real ext-real Element of REAL
y1 / 2 is V31() real ext-real Element of REAL
(y2 `1) - (y1 / 2) is V31() real ext-real Element of REAL
y2 `2 is V31() real ext-real Element of REAL
y2 . 2 is V31() real ext-real Element of REAL
|[((y2 `1) - (y1 / 2)),(y2 `2)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
a is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
a `1 is V31() real ext-real Element of REAL
a . 1 is V31() real ext-real Element of REAL
b is Element of the carrier of (Euclid 2)
dist (x1,b) is V31() real ext-real Element of REAL
(Pitag_dist 2) . (x1,b) is set
[x1,b] is set
{x1,b} is non empty finite set
{x1} is non empty finite set
{{x1,b},{x1}} is non empty finite V40() set
(Pitag_dist 2) . [x1,b] is V31() real ext-real set
(y2 `1) - (a `1) is V31() real ext-real Element of REAL
((y2 `1) - (a `1)) ^2 is V31() real ext-real Element of REAL
((y2 `1) - (a `1)) * ((y2 `1) - (a `1)) is V31() real ext-real set
a `2 is V31() real ext-real Element of REAL
a . 2 is V31() real ext-real Element of REAL
(y2 `2) - (a `2) is V31() real ext-real Element of REAL
((y2 `2) - (a `2)) ^2 is V31() real ext-real Element of REAL
((y2 `2) - (a `2)) * ((y2 `2) - (a `2)) is V31() real ext-real set
(((y2 `1) - (a `1)) ^2) + (((y2 `2) - (a `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((y2 `1) - (a `1)) ^2) + (((y2 `2) - (a `2)) ^2)) is V31() real ext-real Element of REAL
(y2 `1) - ((y2 `1) - (y1 / 2)) is V31() real ext-real Element of REAL
((y2 `1) - ((y2 `1) - (y1 / 2))) ^2 is V31() real ext-real Element of REAL
((y2 `1) - ((y2 `1) - (y1 / 2))) * ((y2 `1) - ((y2 `1) - (y1 / 2))) is V31() real ext-real set
(((y2 `1) - ((y2 `1) - (y1 / 2))) ^2) + (((y2 `2) - (a `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((y2 `1) - ((y2 `1) - (y1 / 2))) ^2) + (((y2 `2) - (a `2)) ^2)) is V31() real ext-real Element of REAL
(y2 `2) - (y2 `2) is V31() real ext-real Element of REAL
((y2 `2) - (y2 `2)) ^2 is V31() real ext-real Element of REAL
((y2 `2) - (y2 `2)) * ((y2 `2) - (y2 `2)) is V31() real ext-real set
(((y2 `1) - ((y2 `1) - (y1 / 2))) ^2) + (((y2 `2) - (y2 `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((y2 `1) - ((y2 `1) - (y1 / 2))) ^2) + (((y2 `2) - (y2 `2)) ^2)) is V31() real ext-real Element of REAL
(y2 `1) - 0 is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
2 * x1 is V31() real ext-real Element of REAL
x2 is Element of the carrier of (Euclid 2)
Ball (x2,x1) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 `1 is V31() real ext-real Element of REAL
y1 . 1 is V31() real ext-real Element of REAL
(y1 `1) - (2 * x1) is V31() real ext-real Element of REAL
y1 `2 is V31() real ext-real Element of REAL
y1 . 2 is V31() real ext-real Element of REAL
|[((y1 `1) - (2 * x1)),(y1 `2)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
b is Element of the carrier of (Euclid 2)
a is Element of the carrier of (Euclid 2)
dist (b,a) is V31() real ext-real Element of REAL
(Pitag_dist 2) . (b,a) is set
[b,a] is set
{b,a} is non empty finite set
{b} is non empty finite set
{{b,a},{b}} is non empty finite V40() set
(Pitag_dist 2) . [b,a] is V31() real ext-real set
|[((y1 `1) - (2 * x1)),(y1 `2)]| `1 is V31() real ext-real Element of REAL
|[((y1 `1) - (2 * x1)),(y1 `2)]| . 1 is V31() real ext-real Element of REAL
(y1 `1) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `1) is V31() real ext-real Element of REAL
((y1 `1) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `1)) ^2 is V31() real ext-real Element of REAL
((y1 `1) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `1)) * ((y1 `1) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `1)) is V31() real ext-real set
|[((y1 `1) - (2 * x1)),(y1 `2)]| `2 is V31() real ext-real Element of REAL
|[((y1 `1) - (2 * x1)),(y1 `2)]| . 2 is V31() real ext-real Element of REAL
(y1 `2) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `2) is V31() real ext-real Element of REAL
((y1 `2) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `2)) ^2 is V31() real ext-real Element of REAL
((y1 `2) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `2)) * ((y1 `2) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `2)) is V31() real ext-real set
(((y1 `1) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `1)) ^2) + (((y1 `2) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((y1 `1) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `1)) ^2) + (((y1 `2) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `2)) ^2)) is V31() real ext-real Element of REAL
(y1 `1) - ((y1 `1) - (2 * x1)) is V31() real ext-real Element of REAL
((y1 `1) - ((y1 `1) - (2 * x1))) ^2 is V31() real ext-real Element of REAL
((y1 `1) - ((y1 `1) - (2 * x1))) * ((y1 `1) - ((y1 `1) - (2 * x1))) is V31() real ext-real set
(((y1 `1) - ((y1 `1) - (2 * x1))) ^2) + (((y1 `2) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((y1 `1) - ((y1 `1) - (2 * x1))) ^2) + (((y1 `2) - (|[((y1 `1) - (2 * x1)),(y1 `2)]| `2)) ^2)) is V31() real ext-real Element of REAL
0 ^2 is V31() real ext-real Element of REAL
0 * 0 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set
(y1 `1) - (y1 `1) is V31() real ext-real Element of REAL
2 * ((y1 `1) - (y1 `1)) is V31() real ext-real Element of REAL
(2 * ((y1 `1) - (y1 `1))) * (2 * x1) is V31() real ext-real Element of REAL
(0 ^2) + ((2 * ((y1 `1) - (y1 `1))) * (2 * x1)) is V31() real ext-real Element of REAL
(2 * x1) ^2 is V31() real ext-real Element of REAL
(2 * x1) * (2 * x1) is V31() real ext-real set
((0 ^2) + ((2 * ((y1 `1) - (y1 `1))) * (2 * x1))) + ((2 * x1) ^2) is V31() real ext-real Element of REAL
(y1 `2) - (y1 `2) is V31() real ext-real Element of REAL
((y1 `2) - (y1 `2)) ^2 is V31() real ext-real Element of REAL
((y1 `2) - (y1 `2)) * ((y1 `2) - (y1 `2)) is V31() real ext-real set
(((0 ^2) + ((2 * ((y1 `1) - (y1 `1))) * (2 * x1))) + ((2 * x1) ^2)) + (((y1 `2) - (y1 `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((0 ^2) + ((2 * ((y1 `1) - (y1 `1))) * (2 * x1))) + ((2 * x1) ^2)) + (((y1 `2) - (y1 `2)) ^2)) is V31() real ext-real Element of REAL
dist (x2,a) is V31() real ext-real Element of REAL
dist (x2,b) is V31() real ext-real Element of REAL
x1 + x1 is V31() real ext-real Element of REAL
(dist (x2,b)) + (dist (x2,a)) is V31() real ext-real Element of REAL
x1 is V31() real ext-real Element of REAL
x2 is non empty compact bounded Element of bool the carrier of (TOP-REAL 2)
E-bound x2 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x2 is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2
proj1 | x2 is non empty Relation-like the carrier of ((TOP-REAL 2) | x2) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous with_max with_min bounded Element of bool [: the carrier of ((TOP-REAL 2) | x2),REAL:]
the carrier of ((TOP-REAL 2) | x2) is non empty set
[: the carrier of ((TOP-REAL 2) | x2),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x2),REAL:] is non empty set
upper_bound (proj1 | x2) is V31() real ext-real Element of REAL
(proj1 | x2) .: the carrier of ((TOP-REAL 2) | x2) is non empty V202() V203() V204() Element of bool REAL
upper_bound ((proj1 | x2) .: the carrier of ((TOP-REAL 2) | x2)) is V31() real ext-real Element of REAL
abs (E-bound x2) is V31() real ext-real Element of REAL
N-bound x2 is V31() real ext-real Element of REAL
proj2 | x2 is non empty Relation-like the carrier of ((TOP-REAL 2) | x2) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous with_max with_min bounded Element of bool [: the carrier of ((TOP-REAL 2) | x2),REAL:]
upper_bound (proj2 | x2) is V31() real ext-real Element of REAL
(proj2 | x2) .: the carrier of ((TOP-REAL 2) | x2) is non empty V202() V203() V204() Element of bool REAL
upper_bound ((proj2 | x2) .: the carrier of ((TOP-REAL 2) | x2)) is V31() real ext-real Element of REAL
abs (N-bound x2) is V31() real ext-real Element of REAL
(abs (E-bound x2)) + (abs (N-bound x2)) is V31() real ext-real Element of REAL
W-bound x2 is V31() real ext-real Element of REAL
lower_bound (proj1 | x2) is V31() real ext-real Element of REAL
lower_bound ((proj1 | x2) .: the carrier of ((TOP-REAL 2) | x2)) is V31() real ext-real Element of REAL
abs (W-bound x2) is V31() real ext-real Element of REAL
((abs (E-bound x2)) + (abs (N-bound x2))) + (abs (W-bound x2)) is V31() real ext-real Element of REAL
S-bound x2 is V31() real ext-real Element of REAL
lower_bound (proj2 | x2) is V31() real ext-real Element of REAL
lower_bound ((proj2 | x2) .: the carrier of ((TOP-REAL 2) | x2)) is V31() real ext-real Element of REAL
abs (S-bound x2) is V31() real ext-real Element of REAL
(((abs (E-bound x2)) + (abs (N-bound x2))) + (abs (W-bound x2))) + (abs (S-bound x2)) is V31() real ext-real Element of REAL
((((abs (E-bound x2)) + (abs (N-bound x2))) + (abs (W-bound x2))) + (abs (S-bound x2))) + x1 is V31() real ext-real Element of REAL
y1 is Element of the carrier of (Euclid 2)
Ball (y1,(((((abs (E-bound x2)) + (abs (N-bound x2))) + (abs (W-bound x2))) + (abs (S-bound x2))) + x1)) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
((((abs (E-bound x2)) + (abs (N-bound x2))) + (abs (W-bound x2))) + (abs (S-bound x2))) + 0 is V31() real ext-real Element of REAL
B is set
d is Element of the carrier of (Euclid 2)
r is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
r `1 is V31() real ext-real Element of REAL
r . 1 is V31() real ext-real Element of REAL
A is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
A `1 is V31() real ext-real Element of REAL
A . 1 is V31() real ext-real Element of REAL
A `2 is V31() real ext-real Element of REAL
A . 2 is V31() real ext-real Element of REAL
r `2 is V31() real ext-real Element of REAL
r . 2 is V31() real ext-real Element of REAL
dist (y1,d) is V31() real ext-real Element of REAL
(Pitag_dist 2) . (y1,d) is set
[y1,d] is set
{y1,d} is non empty finite set
{y1} is non empty finite set
{{y1,d},{y1}} is non empty finite V40() set
(Pitag_dist 2) . [y1,d] is V31() real ext-real set
(r `1) - (A `1) is V31() real ext-real Element of REAL
((r `1) - (A `1)) ^2 is V31() real ext-real Element of REAL
((r `1) - (A `1)) * ((r `1) - (A `1)) is V31() real ext-real set
(r `2) - (A `2) is V31() real ext-real Element of REAL
((r `2) - (A `2)) ^2 is V31() real ext-real Element of REAL
((r `2) - (A `2)) * ((r `2) - (A `2)) is V31() real ext-real set
(((r `1) - (A `1)) ^2) + (((r `2) - (A `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((r `1) - (A `1)) ^2) + (((r `2) - (A `2)) ^2)) is V31() real ext-real Element of REAL
(A `1) ^2 is V31() real ext-real Element of REAL
(A `1) * (A `1) is V31() real ext-real set
(A `2) ^2 is V31() real ext-real Element of REAL
(A `2) * (A `2) is V31() real ext-real set
((A `1) ^2) + ((A `2) ^2) is V31() real ext-real Element of REAL
sqrt (((A `1) ^2) + ((A `2) ^2)) is V31() real ext-real Element of REAL
sqrt ((A `1) ^2) is V31() real ext-real Element of REAL
sqrt ((A `2) ^2) is V31() real ext-real Element of REAL
(sqrt ((A `1) ^2)) + (sqrt ((A `2) ^2)) is V31() real ext-real Element of REAL
abs (A `1) is V31() real ext-real Element of REAL
(abs (A `1)) + (sqrt ((A `2) ^2)) is V31() real ext-real Element of REAL
abs (A `2) is V31() real ext-real Element of REAL
(abs (A `1)) + (abs (A `2)) is V31() real ext-real Element of REAL
((abs (E-bound x2)) + (abs (N-bound x2))) + 0 is V31() real ext-real Element of REAL
(abs (N-bound x2)) + (abs (W-bound x2)) is V31() real ext-real Element of REAL
0 + ((abs (N-bound x2)) + (abs (W-bound x2))) is V31() real ext-real Element of REAL
(abs (E-bound x2)) + ((abs (N-bound x2)) + (abs (W-bound x2))) is V31() real ext-real Element of REAL
(abs (W-bound x2)) + (abs (N-bound x2)) is V31() real ext-real Element of REAL
((abs (E-bound x2)) + (abs (N-bound x2))) + (abs (S-bound x2)) is V31() real ext-real Element of REAL
(((abs (E-bound x2)) + (abs (N-bound x2))) + (abs (S-bound x2))) + 0 is V31() real ext-real Element of REAL
(((abs (E-bound x2)) + (abs (N-bound x2))) + (abs (S-bound x2))) + (abs (W-bound x2)) is V31() real ext-real Element of REAL
(abs (E-bound x2)) + (abs (S-bound x2)) is V31() real ext-real Element of REAL
((abs (E-bound x2)) + (abs (S-bound x2))) + 0 is V31() real ext-real Element of REAL
((abs (E-bound x2)) + (abs (S-bound x2))) + (abs (N-bound x2)) is V31() real ext-real Element of REAL
(abs (W-bound x2)) + (abs (S-bound x2)) is V31() real ext-real Element of REAL
0 + ((abs (W-bound x2)) + (abs (S-bound x2))) is V31() real ext-real Element of REAL
((abs (E-bound x2)) + (abs (N-bound x2))) + ((abs (W-bound x2)) + (abs (S-bound x2))) is V31() real ext-real Element of REAL
x1 is V31() real ext-real set
x2 is non empty Reflexive symmetric triangle MetrStruct
the carrier of x2 is non empty set
y1 is Element of the carrier of x2
Sphere (y1,x1) is Element of bool the carrier of x2
bool the carrier of x2 is non empty set
y2 is set
a is Element of the carrier of x2
dist (a,y1) is V31() real ext-real Element of REAL
x1 is non empty Reflexive discerning MetrStruct
the carrier of x1 is non empty set
x2 is Element of the carrier of x1
Sphere (x2,0) is Element of bool the carrier of x1
bool the carrier of x1 is non empty set
{x2} is non empty finite set
y1 is set
y2 is Element of the carrier of x1
dist (x2,y2) is V31() real ext-real Element of REAL
y1 is set
dist (x2,x2) is V31() real ext-real Element of REAL
x1 is V31() real ext-real set
x2 is non empty Reflexive symmetric triangle MetrStruct
the carrier of x2 is non empty set
y1 is Element of the carrier of x2
cl_Ball (y1,x1) is Element of bool the carrier of x2
bool the carrier of x2 is non empty set
Sphere (y1,x1) is Element of bool the carrier of x2
Ball (y1,x1) is bounded Element of bool the carrier of x2
(Sphere (y1,x1)) \/ (Ball (y1,x1)) is Element of bool the carrier of x2
x1 is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of x1 is non empty set
x2 is Element of the carrier of x1
cl_Ball (x2,0) is Element of bool the carrier of x1
bool the carrier of x1 is non empty set
{x2} is non empty finite set
y1 is set
y2 is Element of the carrier of x1
dist (y2,x2) is V31() real ext-real Element of REAL
y1 is set
dist (x2,x2) is V31() real ext-real Element of REAL
x1 is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of x1 is non empty set
TopSpaceMetr x1 is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr x1) is non empty set
bool the carrier of (TopSpaceMetr x1) is non empty set
x2 is Element of the carrier of x1
y1 is V31() real ext-real set
cl_Ball (x2,y1) is Element of bool the carrier of x1
bool the carrier of x1 is non empty set
y2 is Element of bool the carrier of (TopSpaceMetr x1)
y2 ` is Element of bool the carrier of (TopSpaceMetr x1)
the carrier of (TopSpaceMetr x1) \ y2 is set
a is set
b is Element of the carrier of x1
dist (b,x2) is V31() real ext-real Element of REAL
(dist (b,x2)) - y1 is V31() real ext-real Element of REAL
Ball (b,((dist (b,x2)) - y1)) is bounded Element of bool the carrier of x1
O is Element of bool the carrier of (TopSpaceMetr x1)
g is set
g is Element of the carrier of x1
dist (b,g) is V31() real ext-real Element of REAL
dist (g,x2) is V31() real ext-real Element of REAL
(dist (b,g)) + (dist (g,x2)) is V31() real ext-real Element of REAL
((dist (b,g)) + (dist (g,x2))) - y1 is V31() real ext-real Element of REAL
(((dist (b,g)) + (dist (g,x2))) - y1) - (dist (b,g)) is V31() real ext-real Element of REAL
(dist (b,g)) - (dist (b,g)) is V31() real ext-real Element of REAL
((dist (b,g)) - (dist (b,g))) + (dist (g,x2)) is V31() real ext-real Element of REAL
(((dist (b,g)) - (dist (b,g))) + (dist (g,x2))) - y1 is V31() real ext-real Element of REAL
dist (x2,b) is V31() real ext-real Element of REAL
y1 - y1 is V31() real ext-real set
b is Element of bool the carrier of (TopSpaceMetr x1)
x1 is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of x1 is non empty set
TopSpaceMetr x1 is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr x1) is non empty set
bool the carrier of (TopSpaceMetr x1) is non empty set
x2 is Element of the carrier of x1
y1 is V31() real ext-real set
cl_Ball (x2,y1) is Element of bool the carrier of x1
bool the carrier of x1 is non empty set
y2 is Element of bool the carrier of (TopSpaceMetr x1)
y2 ` is Element of bool the carrier of (TopSpaceMetr x1)
the carrier of (TopSpaceMetr x1) \ y2 is set
x1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
Euclid x1 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL x1 is non empty functional FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b<sub>1</sub> = x1 } is set
Pitag_dist x1 is non empty Relation-like [:(REAL x1),(REAL x1):] -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:[:(REAL x1),(REAL x1):],REAL:]
[:(REAL x1),(REAL x1):] is non empty set
[:[:(REAL x1),(REAL x1):],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:(REAL x1),(REAL x1):],REAL:] is non empty set
MetrStruct(# (REAL x1),(Pitag_dist x1) #) is strict MetrStruct
the carrier of (Euclid x1) is non empty set
TOP-REAL x1 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL x1) is non empty set
bool the carrier of (TOP-REAL x1) is non empty set
x2 is Element of the carrier of (Euclid x1)
y1 is Element of bool the carrier of (TOP-REAL x1)
y2 is V31() real ext-real set
cl_Ball (x2,y2) is Element of bool the carrier of (Euclid x1)
bool the carrier of (Euclid x1) is non empty set
the topology of (TOP-REAL x1) is non empty open Element of bool (bool the carrier of (TOP-REAL x1))
bool (bool the carrier of (TOP-REAL x1)) is non empty set
TopStruct(# the carrier of (TOP-REAL x1), the topology of (TOP-REAL x1) #) is non empty strict TopSpace-like TopStruct
TopSpaceMetr (Euclid x1) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid x1)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid x1)) is non empty set
a is Element of bool the carrier of (TopSpaceMetr (Euclid x1))
x1 is V31() real ext-real set
x2 is non empty Reflexive symmetric triangle MetrStruct
the carrier of x2 is non empty set
y1 is Element of the carrier of x2
cl_Ball (y1,x1) is Element of bool the carrier of x2
bool the carrier of x2 is non empty set
x1 + 1 is V31() real ext-real Element of REAL
Ball (y1,(x1 + 1)) is bounded Element of bool the carrier of x2
y2 is set
x1 + 0 is V31() real ext-real Element of REAL
a is Element of the carrier of x2
dist (y1,a) is V31() real ext-real Element of REAL
x1 is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of x1 is non empty set
TopSpaceMetr x1 is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr x1) is non empty set
bool the carrier of (TopSpaceMetr x1) is non empty set
x2 is Element of the carrier of x1
y1 is V31() real ext-real set
Sphere (x2,y1) is Element of bool the carrier of x1
bool the carrier of x1 is non empty set
y2 is Element of bool the carrier of (TopSpaceMetr x1)
cl_Ball (x2,y1) is Element of bool the carrier of x1
Ball (x2,y1) is bounded Element of bool the carrier of x1
(cl_Ball (x2,y1)) ` is Element of bool the carrier of x1
the carrier of x1 \ (cl_Ball (x2,y1)) is set
a is Element of bool the carrier of (TopSpaceMetr x1)
a ` is Element of bool the carrier of (TopSpaceMetr x1)
the carrier of (TopSpaceMetr x1) \ a is set
y2 ` is Element of bool the carrier of (TopSpaceMetr x1)
the carrier of (TopSpaceMetr x1) \ y2 is set
b is Element of bool the carrier of (TopSpaceMetr x1)
(a `) \/ b is Element of bool the carrier of (TopSpaceMetr x1)
O is set
g is Element of the carrier of x1
dist (g,x2) is V31() real ext-real Element of REAL
O is set
g is Element of the carrier of x1
dist (g,x2) is V31() real ext-real Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
Euclid x1 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL x1 is non empty functional FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b<sub>1</sub> = x1 } is set
Pitag_dist x1 is non empty Relation-like [:(REAL x1),(REAL x1):] -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:[:(REAL x1),(REAL x1):],REAL:]
[:(REAL x1),(REAL x1):] is non empty set
[:[:(REAL x1),(REAL x1):],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:(REAL x1),(REAL x1):],REAL:] is non empty set
MetrStruct(# (REAL x1),(Pitag_dist x1) #) is strict MetrStruct
the carrier of (Euclid x1) is non empty set
TOP-REAL x1 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL x1) is non empty set
bool the carrier of (TOP-REAL x1) is non empty set
x2 is Element of the carrier of (Euclid x1)
y1 is Element of bool the carrier of (TOP-REAL x1)
y2 is V31() real ext-real set
Sphere (x2,y2) is Element of bool the carrier of (Euclid x1)
bool the carrier of (Euclid x1) is non empty set
the topology of (TOP-REAL x1) is non empty open Element of bool (bool the carrier of (TOP-REAL x1))
bool (bool the carrier of (TOP-REAL x1)) is non empty set
TopStruct(# the carrier of (TOP-REAL x1), the topology of (TOP-REAL x1) #) is non empty strict TopSpace-like TopStruct
TopSpaceMetr (Euclid x1) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid x1)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid x1)) is non empty set
a is Element of bool the carrier of (TopSpaceMetr (Euclid x1))
x1 is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of x1 is non empty set
x2 is Element of the carrier of x1
y1 is V31() real ext-real set
Sphere (x2,y1) is Element of bool the carrier of x1
bool the carrier of x1 is non empty set
cl_Ball (x2,y1) is Element of bool the carrier of x1
x1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
TOP-REAL x1 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL x1) is non empty set
bool the carrier of (TOP-REAL x1) is non empty set
x2 is Element of bool the carrier of (TOP-REAL x1)
Cl x2 is closed Element of bool the carrier of (TOP-REAL x1)
x1 is non empty MetrStruct
the carrier of x1 is non empty set
bool the carrier of x1 is non empty set
[#] x1 is non empty non proper Element of bool the carrier of x1
x2 is Element of bool the carrier of x1
x1 is non empty Reflexive symmetric triangle MetrStruct
the carrier of x1 is non empty set
bool the carrier of x1 is non empty set
x2 is Element of bool the carrier of x1
y1 is Element of bool the carrier of x1
x2 \/ y1 is Element of bool the carrier of x1
[#] x1 is non empty non proper Element of bool the carrier of x1
x1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
TOP-REAL x1 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL x1) is non empty set
bool the carrier of (TOP-REAL x1) is non empty set
y1 is Element of bool the carrier of (TOP-REAL x1)
y2 is Element of bool the carrier of (TOP-REAL x1)
y1 \/ y2 is Element of bool the carrier of (TOP-REAL x1)
Euclid x1 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL x1 is non empty functional FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b<sub>1</sub> = x1 } is set
Pitag_dist x1 is non empty Relation-like [:(REAL x1),(REAL x1):] -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:[:(REAL x1),(REAL x1):],REAL:]
[:(REAL x1),(REAL x1):] is non empty set
[:[:(REAL x1),(REAL x1):],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:(REAL x1),(REAL x1):],REAL:] is non empty set
MetrStruct(# (REAL x1),(Pitag_dist x1) #) is strict MetrStruct
the carrier of (Euclid x1) is non empty set
bool the carrier of (Euclid x1) is non empty set
[#] (TOP-REAL x1) is non empty non proper non proper open open closed closed dense dense non boundary non boundary connected a_component convex Element of bool the carrier of (TOP-REAL x1)
a is Element of bool the carrier of (Euclid x1)
O is bounded Element of bool the carrier of (Euclid x1)
b is Element of bool the carrier of (Euclid x1)
O \/ b is Element of bool the carrier of (Euclid x1)
[#] (Euclid x1) is non empty non proper Element of bool the carrier of (Euclid x1)
x1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
TOP-REAL x1 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL x1) is non empty set
bool the carrier of (TOP-REAL x1) is non empty set
x2 is Element of bool the carrier of (TOP-REAL x1)
y1 is Element of bool the carrier of (TOP-REAL x1)
x2 \/ y1 is Element of bool the carrier of (TOP-REAL x1)
Euclid x1 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL x1 is non empty functional FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b<sub>1</sub> = x1 } is set
Pitag_dist x1 is non empty Relation-like [:(REAL x1),(REAL x1):] -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:[:(REAL x1),(REAL x1):],REAL:]
[:(REAL x1),(REAL x1):] is non empty set
[:[:(REAL x1),(REAL x1):],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:(REAL x1),(REAL x1):],REAL:] is non empty set
MetrStruct(# (REAL x1),(Pitag_dist x1) #) is strict MetrStruct
the carrier of (Euclid x1) is non empty set
bool the carrier of (Euclid x1) is non empty set
y2 is Element of bool the carrier of (Euclid x1)
a is Element of bool the carrier of (Euclid x1)
y2 \/ a is Element of bool the carrier of (Euclid x1)
b is Element of bool the carrier of (Euclid x1)
x1 is non empty V202() V203() V204() Element of bool REAL
Cl x1 is closed V202() V203() V204() Element of bool REAL
x1 is V202() V203() V204() bounded_below Element of bool REAL
Cl x1 is closed V202() V203() V204() Element of bool REAL
x2 is V31() real ext-real set
y1 is V31() real ext-real set
y1 is ext-real set
y2 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:NAT,REAL:]
rng y2 is V202() V203() V204() Element of bool REAL
lim y2 is V31() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
y2 . a is V31() real ext-real Element of REAL
dom y2 is V202() V203() V204() V205() V206() V207() bounded_below Element of bool NAT
x1 is V202() V203() V204() bounded_above Element of bool REAL
Cl x1 is closed V202() V203() V204() Element of bool REAL
x2 is V31() real ext-real set
y1 is V31() real ext-real set
y1 is ext-real set
y2 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:NAT,REAL:]
rng y2 is V202() V203() V204() Element of bool REAL
lim y2 is V31() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
y2 . a is V31() real ext-real Element of REAL
dom y2 is V202() V203() V204() V205() V206() V207() bounded_below Element of bool NAT
x1 is non empty V202() V203() V204() bounded_below Element of bool REAL
lower_bound x1 is V31() real ext-real Element of REAL
Cl x1 is non empty closed V202() V203() V204() bounded_below Element of bool REAL
lower_bound (Cl x1) is V31() real ext-real Element of REAL
x2 is V31() real ext-real set
y1 is V31() real ext-real set
y2 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:NAT,REAL:]
rng y2 is V202() V203() V204() Element of bool REAL
lim y2 is V31() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
y2 . a is V31() real ext-real Element of REAL
dom y2 is V202() V203() V204() V205() V206() V207() bounded_below Element of bool NAT
x2 is V31() real ext-real set
x1 is non empty V202() V203() V204() bounded_above Element of bool REAL
upper_bound x1 is V31() real ext-real Element of REAL
Cl x1 is non empty closed V202() V203() V204() bounded_above Element of bool REAL
upper_bound (Cl x1) is V31() real ext-real Element of REAL
x2 is V31() real ext-real set
y1 is V31() real ext-real set
y2 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:NAT,REAL:]
rng y2 is V202() V203() V204() Element of bool REAL
lim y2 is V31() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
y2 . a is V31() real ext-real Element of REAL
dom y2 is V202() V203() V204() V205() V206() V207() bounded_below Element of bool NAT
x2 is V31() real ext-real 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 set
bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):] is non empty set
x1 is V202() V203() V204() Element of bool REAL
x2 is V202() V203() V204() Element of bool REAL
[:x1,x2:] is complex-yielding V193() V194() set
(1,2) --> (x1,x2) is non empty Relation-like NAT -defined {1,2} -defined bool REAL -valued Function-like total quasi_total finite Element of bool [:{1,2},(bool REAL):]
[:{1,2},(bool REAL):] is non empty set
bool [:{1,2},(bool REAL):] is non empty set
product ((1,2) --> (x1,x2)) is set
y1 is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
y1 .: [:x1,x2:] is Element of bool the carrier of (TOP-REAL 2)
dom ((1,2) --> (x1,x2)) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool {1,2}
bool {1,2} is non empty finite V40() set
a is set
b is set
y1 . b is set
O is Element of the carrier of [:R^1,R^1:]
g is set
g is set
[g,g] is set
{g,g} is non empty finite set
{g} is non empty finite set
{{g,g},{g}} is non empty finite V40() set
y1 . O is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
[:(Seg 2),REAL:] is non empty complex-yielding V193() V194() set
bool [:(Seg 2),REAL:] is non empty set
B is non empty Relation-like Seg 2 -defined REAL -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg 2),REAL:]
A is set
B . A is V31() real ext-real Element of REAL
((1,2) --> (x1,x2)) . A is set
d is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
|[d,r]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|[d,r]| `1 is V31() real ext-real Element of REAL
|[d,r]| . 1 is V31() real ext-real Element of REAL
|[d,r]| `2 is V31() real ext-real Element of REAL
|[d,r]| . 2 is V31() real ext-real Element of REAL
[d,r] is set
{d,r} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{d} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{d,r},{d}} is non empty finite V40() set
y1 . [d,r] is set
dom B is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool (Seg 2)
bool (Seg 2) is non empty finite V40() set
((1,2) --> (x1,x2)) . 2 is set
a is set
b is Relation-like Function-like set
dom b is set
b . 2 is set
((1,2) --> (x1,x2)) . 1 is set
b . 1 is set
[(b . 1),(b . 2)] is set
{(b . 1),(b . 2)} is non empty finite set
{(b . 1)} is non empty finite set
{{(b . 1),(b . 2)},{(b . 1)}} is non empty finite V40() set
y1 . [(b . 1),(b . 2)] is set
<*(b . 1),(b . 2)*> is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like set
O is set
b . O is set
<*(b . 1),(b . 2)*> . O is set
dom <*(b . 1),(b . 2)*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT
[: the carrier of R^1, the carrier of R^1:] is non empty complex-yielding V193() V194() set
[: the carrier of (TOP-REAL 2), the carrier of R^1:] is non empty complex-yielding V193() V194() set
bool [: the carrier of (TOP-REAL 2), the carrier of R^1:] is non empty set
y1 is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
dom y1 is Element of bool the carrier of [:R^1,R^1:]
bool the carrier of [:R^1,R^1:] is non empty set
[#] [:R^1,R^1:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:R^1,R^1:]
rng y1 is Element of bool the carrier of (TOP-REAL 2)
[#] (TOP-REAL 2) is non empty non proper non proper open open closed closed dense dense non boundary non boundary connected a_component being_Region convex Element of bool the carrier of (TOP-REAL 2)
y1 " is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of [:R^1,R^1:] -valued Function-like total quasi_total Element of bool [: the carrier of (TOP-REAL 2), the carrier of [:R^1,R^1:]:]
[: the carrier of (TOP-REAL 2), the carrier of [:R^1,R^1:]:] is non empty set
bool [: the carrier of (TOP-REAL 2), the carrier of [:R^1,R^1:]:] is non empty set
[: the carrier of R^1, the carrier of R^1:] is non empty complex-yielding V193() V194() set
y2 is set
a is V31() real ext-real Element of REAL
b is V31() real ext-real Element of REAL
<*a,b*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
[a,b] is set
{a,b} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{a} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{a,b},{a}} is non empty finite V40() set
y1 . [a,b] is set
y2 is set
dom y1 is set
a is set
y1 . y2 is set
y1 . a is set
b is set
O is set
[b,O] is set
{b,O} is non empty finite set
{b} is non empty finite set
{{b,O},{b}} is non empty finite V40() set
g is set
g is set
[g,g] is set
{g,g} is non empty finite set
{g} is non empty finite set
{{g,g},{g}} is non empty finite V40() set
r is V31() real ext-real Element of REAL
A is V31() real ext-real Element of REAL
[r,A] is set
{r,A} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{r} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{r,A},{r}} is non empty finite V40() set
y1 . [r,A] is set
<*r,A*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
B is V31() real ext-real Element of REAL
d is V31() real ext-real Element of REAL
[B,d] is set
{B,d} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{B} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{B,d},{B}} is non empty finite V40() set
y1 . [B,d] is set
<*B,d*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
x2 is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [: the carrier of (TOP-REAL 2), the carrier of R^1:]
dom x2 is Element of bool the carrier of (TOP-REAL 2)
x1 is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [: the carrier of (TOP-REAL 2), the carrier of R^1:]
dom x1 is Element of bool the carrier of (TOP-REAL 2)
y2 is set
dom (y1 ") is Element of bool the carrier of (TOP-REAL 2)
a is V31() real ext-real Element of REAL
b is V31() real ext-real Element of REAL
<*a,b*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
[a,b] is set
{a,b} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{a} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{a,b},{a}} is non empty finite V40() set
y1 . [a,b] is set
(y1 ") . y2 is set
y1 " is Relation-like Function-like set
(y1 ") . y2 is set
O is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
O `1 is V31() real ext-real Element of REAL
O . 1 is V31() real ext-real Element of REAL
[(O `1),b] is set
{(O `1),b} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{(O `1)} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{(O `1),b},{(O `1)}} is non empty finite V40() set
O `2 is V31() real ext-real Element of REAL
O . 2 is V31() real ext-real Element of REAL
[(O `1),(O `2)] is set
{(O `1),(O `2)} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{(O `1),(O `2)},{(O `1)}} is non empty finite V40() set
x1 . y2 is V31() real ext-real Element of REAL
[(x1 . y2),(O `2)] is set
{(x1 . y2),(O `2)} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{(x1 . y2)} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{(x1 . y2),(O `2)},{(x1 . y2)}} is non empty finite V40() set
x2 . y2 is V31() real ext-real Element of REAL
[(x1 . y2),(x2 . y2)] is set
{(x1 . y2),(x2 . y2)} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{(x1 . y2),(x2 . y2)},{(x1 . y2)}} is non empty finite V40() set
<:x1,x2:> is non empty Relation-like the carrier of (TOP-REAL 2) -defined [: the carrier of R^1, the carrier of R^1:] -valued Function-like total quasi_total Element of bool [: the carrier of (TOP-REAL 2),[: the carrier of R^1, the carrier of R^1:]:]
[: the carrier of (TOP-REAL 2),[: the carrier of R^1, the carrier of R^1:]:] is non empty set
bool [: the carrier of (TOP-REAL 2),[: the carrier of R^1, the carrier of R^1:]:] is non empty set
<:x1,x2:> . y2 is set
y2 is Element of the carrier of [:R^1,R^1:]
y1 . y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
a is non empty a_neighborhood of y1 . y2
O is set
g is set
[O,g] is set
{O,g} is non empty finite set
{O} is non empty finite set
{{O,g},{O}} is non empty finite V40() set
b is Element of the carrier of (Euclid 2)
Int a is open Element of bool the carrier of (TOP-REAL 2)
d is V31() real ext-real set
Ball (b,d) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
(y1 . y2) `1 is V31() real ext-real Element of REAL
(y1 . y2) . 1 is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
r / (sqrt 2) is V31() real ext-real Element of REAL
((y1 . y2) `1) - (r / (sqrt 2)) is V31() real ext-real Element of REAL
((y1 . y2) `1) + (r / (sqrt 2)) is V31() real ext-real Element of REAL
].(((y1 . y2) `1) - (r / (sqrt 2))),(((y1 . y2) `1) + (r / (sqrt 2))).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
(y1 . y2) `2 is V31() real ext-real Element of REAL
(y1 . y2) . 2 is V31() real ext-real Element of REAL
((y1 . y2) `2) - (r / (sqrt 2)) is V31() real ext-real Element of REAL
((y1 . y2) `2) + (r / (sqrt 2)) is V31() real ext-real Element of REAL
].(((y1 . y2) `2) - (r / (sqrt 2))),(((y1 . y2) `2) + (r / (sqrt 2))).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
g is V31() real ext-real Element of REAL
B is V31() real ext-real Element of REAL
[g,B] is set
{g,B} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{g} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{g,B},{g}} is non empty finite V40() set
y1 . [g,B] is set
<*g,B*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
B is V202() V203() V204() Element of bool the carrier of R^1
A is V202() V203() V204() Element of bool the carrier of R^1
[:A,B:] is complex-yielding V193() V194() Element of bool the carrier of [:R^1,R^1:]
y1 .: [:A,B:] is Element of bool the carrier of (TOP-REAL 2)
Base-Appr [:A,B:] is open Element of bool (bool the carrier of [:R^1,R^1:])
bool (bool the carrier of [:R^1,R^1:]) is non empty set
{ [:b₁,b₂:] where b₁, b₂ is Element of bool the carrier of R^1 : ( [:b₁,b₂:] c= [:A,B:] & b₁ is open & b₂ is open ) } is set
union (Base-Appr [:A,B:]) is Element of bool the carrier of [:R^1,R^1:]
Int [:A,B:] is open Element of bool the carrier of [:R^1,R^1:]
(1,2) --> (A,B) is non empty Relation-like NAT -defined {1,2} -defined bool the carrier of R^1 -valued Function-like total quasi_total finite Element of bool [:{1,2},(bool the carrier of R^1):]
[:{1,2},(bool the carrier of R^1):] is non empty set
bool [:{1,2},(bool the carrier of R^1):] is non empty set
product ((1,2) --> (A,B)) is set
Ball (b,r) is bounded Element of bool the carrier of (Euclid 2)
dom <:x1,x2:> is Element of bool the carrier of (TOP-REAL 2)
x1 is V31() real ext-real Element of REAL
x2 is V31() real ext-real Element of REAL
<*x1,x2*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
[:[:REAL,REAL:],(REAL 2):] is non empty set
bool [:[:REAL,REAL:],(REAL 2):] is non empty set
x1 is non empty Relation-like [:REAL,REAL:] -defined REAL 2 -valued Function-like total quasi_total Element of bool [:[:REAL,REAL:],(REAL 2):]
[: the carrier of R^1, the carrier of R^1:] is non empty complex-yielding V193() V194() set
x2 is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
y1 is V31() real ext-real Element of REAL
y2 is V31() real ext-real Element of REAL
[y1,y2] is set
{y1,y2} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{y1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{y1,y2},{y1}} is non empty finite V40() set
x2 . [y1,y2] is set
<*y1,y2*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
x2 . (y1,y2) is set
a is Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of REAL 2
x1 is compact closed V202() V203() V204() Element of bool REAL
x2 is compact closed V202() V203() V204() Element of bool REAL
(1,2) --> (x1,x2) is non empty Relation-like NAT -defined {1,2} -defined bool REAL -valued Function-like total quasi_total finite Element of bool [:{1,2},(bool REAL):]
[:{1,2},(bool REAL):] is non empty set
bool [:{1,2},(bool REAL):] is non empty set
product ((1,2) --> (x1,x2)) is set
b is V31() real ext-real Element of REAL
O is V31() real ext-real Element of REAL
<*b,O*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
[:[:REAL,REAL:],(REAL 2):] is non empty set
bool [:[:REAL,REAL:],(REAL 2):] is non empty set
b is non empty Relation-like [:REAL,REAL:] -defined REAL 2 -valued Function-like total quasi_total Element of bool [:[:REAL,REAL:],(REAL 2):]
[: the carrier of R^1, the carrier of R^1:] is non empty complex-yielding V193() V194() set
O is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
g is V31() real ext-real Element of REAL
g is V31() real ext-real Element of REAL
[g,g] is set
{g,g} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{g} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set
{{g,g},{g}} is non empty finite V40() set
O . [g,g] is set
<*g,g*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL
O . (g,g) is set
B is Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of REAL 2
a is V202() V203() V204() Element of bool the carrier of R^1
y2 is V202() V203() V204() Element of bool the carrier of R^1
[:y2,a:] is complex-yielding V193() V194() Element of bool the carrier of [:R^1,R^1:]
bool the carrier of [:R^1,R^1:] is non empty set
O .: [:y2,a:] is Element of bool the carrier of (TOP-REAL 2)
y1 is Element of bool the carrier of (TOP-REAL 2)
x1 is Element of bool the carrier of (TOP-REAL 2)
bool the carrier of (Euclid 2) is non empty set
x2 is bounded Element of bool the carrier of (Euclid 2)
y1 is V31() real ext-real Element of REAL
y2 is Element of the carrier of (Euclid 2)
Ball (y2,y1) is bounded Element of bool the carrier of (Euclid 2)
a is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
a `2 is V31() real ext-real Element of REAL
a . 2 is V31() real ext-real Element of REAL
(a `2) - y1 is V31() real ext-real Element of REAL
(a `2) + y1 is V31() real ext-real Element of REAL
].((a `2) - y1),((a `2) + y1).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
[.((a `2) - y1),((a `2) + y1).] is compact closed V202() V203() V204() bounded_below bounded_above real-bounded V280() Element of bool REAL
a `1 is V31() real ext-real Element of REAL
a . 1 is V31() real ext-real Element of REAL
(a `1) - y1 is V31() real ext-real Element of REAL
(a `1) + y1 is V31() real ext-real Element of REAL
].((a `1) - y1),((a `1) + y1).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
(1,2) --> (].((a `1) - y1),((a `1) + y1).[,].((a `2) - y1),((a `2) + y1).[) is non empty Relation-like NAT -defined {1,2} -defined bool REAL -valued Function-like total quasi_total finite Element of bool [:{1,2},(bool REAL):]
[:{1,2},(bool REAL):] is non empty set
bool [:{1,2},(bool REAL):] is non empty set
product ((1,2) --> (].((a `1) - y1),((a `1) + y1).[,].((a `2) - y1),((a `2) + y1).[)) is set
[.((a `1) - y1),((a `1) + y1).] is compact closed V202() V203() V204() bounded_below bounded_above real-bounded V280() Element of bool REAL
(1,2) --> ([.((a `1) - y1),((a `1) + y1).],[.((a `2) - y1),((a `2) + y1).]) is non empty Relation-like NAT -defined {1,2} -defined bool REAL -valued Function-like total quasi_total finite Element of bool [:{1,2},(bool REAL):]
product ((1,2) --> ([.((a `1) - y1),((a `1) + y1).],[.((a `2) - y1),((a `2) + y1).])) is set
x1 is Element of bool the carrier of (TOP-REAL 2)
Cl x1 is closed Element of bool the carrier of (TOP-REAL 2)
x2 is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]
x2 .: x1 is V202() V203() V204() Element of bool REAL
Cl (x2 .: x1) is closed V202() V203() V204() Element of bool REAL
x2 .: (Cl x1) is V202() V203() V204() Element of bool REAL
[: the carrier of (TOP-REAL 2), the carrier of R^1:] is non empty complex-yielding V193() V194() set
bool [: the carrier of (TOP-REAL 2), the carrier of R^1:] is non empty set
y1 is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [: the carrier of (TOP-REAL 2), the carrier of R^1:]
y1 .: (Cl x1) is V202() V203() V204() Element of bool the carrier of R^1
x1 is Element of bool the carrier of (TOP-REAL 2)
Cl x1 is closed Element of bool the carrier of (TOP-REAL 2)
proj1 .: (Cl x1) is V202() V203() V204() Element of bool REAL
proj1 .: x1 is V202() V203() V204() Element of bool REAL
Cl (proj1 .: x1) is closed V202() V203() V204() Element of bool REAL
x2 is set
y1 is set
proj1 . y1 is V31() real ext-real Element of REAL
y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
proj1 . y2 is V31() real ext-real Element of REAL
O is open V202() V203() V204() Element of bool REAL
O /\ (proj1 .: x1) is V202() V203() V204() Element of bool REAL
g is V31() real ext-real set
(proj1 . y2) - g is V31() real ext-real Element of REAL
(proj1 . y2) + g is V31() real ext-real Element of REAL
].((proj1 . y2) - g),((proj1 . y2) + g).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
b is Element of the carrier of (Euclid 2)
g is V31() real ext-real Element of REAL
g / 2 is V31() real ext-real Element of REAL
Ball (b,(g / 2)) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
B is Element of bool the carrier of (TOP-REAL 2)
x1 /\ B is Element of bool the carrier of (TOP-REAL 2)
d is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
d `1 is V31() real ext-real Element of REAL
d . 1 is V31() real ext-real Element of REAL
y2 `1 is V31() real ext-real Element of REAL
y2 . 1 is V31() real ext-real Element of REAL
(y2 `1) - (g / 2) is V31() real ext-real Element of REAL
(proj1 . y2) - (g / 2) is V31() real ext-real Element of REAL
(y2 `1) + (g / 2) is V31() real ext-real Element of REAL
(proj1 . y2) + (g / 2) is V31() real ext-real Element of REAL
proj1 . d is V31() real ext-real Element of REAL
g / 1 is V31() real ext-real Element of REAL
(proj1 . y2) - g is V31() real ext-real Element of REAL
(proj1 . y2) + g is V31() real ext-real Element of REAL
].((proj1 . y2) - g),((proj1 . y2) + g).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
{ b₁ where b₁ is V31() real ext-real Element of REAL : ( not b₁ <= (proj1 . y2) - g & not (proj1 . y2) + g <= b₁ ) } is set
x1 is Element of bool the carrier of (TOP-REAL 2)
Cl x1 is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (Cl x1) is V202() V203() V204() Element of bool REAL
proj2 .: x1 is V202() V203() V204() Element of bool REAL
Cl (proj2 .: x1) is closed V202() V203() V204() Element of bool REAL
x2 is set
y1 is set
proj2 . y1 is V31() real ext-real Element of REAL
y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
proj2 . y2 is V31() real ext-real Element of REAL
O is open V202() V203() V204() Element of bool REAL
O /\ (proj2 .: x1) is V202() V203() V204() Element of bool REAL
g is V31() real ext-real set
(proj2 . y2) - g is V31() real ext-real Element of REAL
(proj2 . y2) + g is V31() real ext-real Element of REAL
].((proj2 . y2) - g),((proj2 . y2) + g).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
b is Element of the carrier of (Euclid 2)
g is V31() real ext-real Element of REAL
g / 2 is V31() real ext-real Element of REAL
Ball (b,(g / 2)) is bounded Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is non empty set
B is Element of bool the carrier of (TOP-REAL 2)
x1 /\ B is Element of bool the carrier of (TOP-REAL 2)
d is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
d `2 is V31() real ext-real Element of REAL
d . 2 is V31() real ext-real Element of REAL
y2 `2 is V31() real ext-real Element of REAL
y2 . 2 is V31() real ext-real Element of REAL
(y2 `2) - (g / 2) is V31() real ext-real Element of REAL
(proj2 . y2) - (g / 2) is V31() real ext-real Element of REAL
(y2 `2) + (g / 2) is V31() real ext-real Element of REAL
(proj2 . y2) + (g / 2) is V31() real ext-real Element of REAL
proj2 . d is V31() real ext-real Element of REAL
g / 1 is V31() real ext-real Element of REAL
(proj2 . y2) - g is V31() real ext-real Element of REAL
(proj2 . y2) + g is V31() real ext-real Element of REAL
].((proj2 . y2) - g),((proj2 . y2) + g).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL
{ b₁ where b₁ is V31() real ext-real Element of REAL : ( not b₁ <= (proj2 . y2) - g & not (proj2 . y2) + g <= b₁ ) } is set
x1 is Element of bool the carrier of (TOP-REAL 2)
proj1 .: x1 is V202() V203() V204() Element of bool REAL
Cl (proj1 .: x1) is closed V202() V203() V204() Element of bool REAL
Cl x1 is closed Element of bool the carrier of (TOP-REAL 2)
proj1 .: (Cl x1) is V202() V203() V204() Element of bool REAL
x1 is Element of bool the carrier of (TOP-REAL 2)
proj2 .: x1 is V202() V203() V204() Element of bool REAL
Cl (proj2 .: x1) is closed V202() V203() V204() Element of bool REAL
Cl x1 is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (Cl x1) is V202() V203() V204() Element of bool REAL
x1 is non empty Element of bool the carrier of (TOP-REAL 2)
W-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | x1 is non empty Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is non empty set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
lower_bound (proj1 | x1) is V31() real ext-real Element of REAL
(proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1) is non empty V202() V203() V204() Element of bool REAL
lower_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
Cl x1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
W-bound (Cl x1) is V31() real ext-real Element of REAL
(TOP-REAL 2) | (Cl x1) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | (Cl x1) is non empty Relation-like the carrier of ((TOP-REAL 2) | (Cl x1)) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:]
the carrier of ((TOP-REAL 2) | (Cl x1)) is non empty set
[: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:] is non empty set
lower_bound (proj1 | (Cl x1)) is V31() real ext-real Element of REAL
(proj1 | (Cl x1)) .: the carrier of ((TOP-REAL 2) | (Cl x1)) is non empty V202() V203() V204() Element of bool REAL
lower_bound ((proj1 | (Cl x1)) .: the carrier of ((TOP-REAL 2) | (Cl x1))) is V31() real ext-real Element of REAL
proj1 .: (Cl x1) is non empty V202() V203() V204() Element of bool REAL
proj1 .: x1 is non empty V202() V203() V204() Element of bool REAL
lower_bound (proj1 .: x1) is V31() real ext-real Element of REAL
Cl (proj1 .: x1) is non empty closed V202() V203() V204() Element of bool REAL
lower_bound (Cl (proj1 .: x1)) is V31() real ext-real Element of REAL
lower_bound (proj1 .: (Cl x1)) is V31() real ext-real Element of REAL
x1 is non empty Element of bool the carrier of (TOP-REAL 2)
E-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | x1 is non empty Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is non empty set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
upper_bound (proj1 | x1) is V31() real ext-real Element of REAL
(proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1) is non empty V202() V203() V204() Element of bool REAL
upper_bound ((proj1 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
Cl x1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
E-bound (Cl x1) is V31() real ext-real Element of REAL
(TOP-REAL 2) | (Cl x1) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | (Cl x1) is non empty Relation-like the carrier of ((TOP-REAL 2) | (Cl x1)) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:]
the carrier of ((TOP-REAL 2) | (Cl x1)) is non empty set
[: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:] is non empty set
upper_bound (proj1 | (Cl x1)) is V31() real ext-real Element of REAL
(proj1 | (Cl x1)) .: the carrier of ((TOP-REAL 2) | (Cl x1)) is non empty V202() V203() V204() Element of bool REAL
upper_bound ((proj1 | (Cl x1)) .: the carrier of ((TOP-REAL 2) | (Cl x1))) is V31() real ext-real Element of REAL
proj1 .: (Cl x1) is non empty V202() V203() V204() Element of bool REAL
proj1 .: x1 is non empty V202() V203() V204() Element of bool REAL
upper_bound (proj1 .: x1) is V31() real ext-real Element of REAL
Cl (proj1 .: x1) is non empty closed V202() V203() V204() Element of bool REAL
upper_bound (Cl (proj1 .: x1)) is V31() real ext-real Element of REAL
upper_bound (proj1 .: (Cl x1)) is V31() real ext-real Element of REAL
x1 is non empty Element of bool the carrier of (TOP-REAL 2)
N-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | x1 is non empty Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is non empty set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
upper_bound (proj2 | x1) is V31() real ext-real Element of REAL
(proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1) is non empty V202() V203() V204() Element of bool REAL
upper_bound ((proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
Cl x1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
N-bound (Cl x1) is V31() real ext-real Element of REAL
(TOP-REAL 2) | (Cl x1) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (Cl x1) is non empty Relation-like the carrier of ((TOP-REAL 2) | (Cl x1)) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:]
the carrier of ((TOP-REAL 2) | (Cl x1)) is non empty set
[: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:] is non empty set
upper_bound (proj2 | (Cl x1)) is V31() real ext-real Element of REAL
(proj2 | (Cl x1)) .: the carrier of ((TOP-REAL 2) | (Cl x1)) is non empty V202() V203() V204() Element of bool REAL
upper_bound ((proj2 | (Cl x1)) .: the carrier of ((TOP-REAL 2) | (Cl x1))) is V31() real ext-real Element of REAL
proj2 .: (Cl x1) is non empty V202() V203() V204() Element of bool REAL
proj2 .: x1 is non empty V202() V203() V204() Element of bool REAL
upper_bound (proj2 .: x1) is V31() real ext-real Element of REAL
Cl (proj2 .: x1) is non empty closed V202() V203() V204() Element of bool REAL
upper_bound (Cl (proj2 .: x1)) is V31() real ext-real Element of REAL
upper_bound (proj2 .: (Cl x1)) is V31() real ext-real Element of REAL
x1 is non empty Element of bool the carrier of (TOP-REAL 2)
S-bound x1 is V31() real ext-real Element of REAL
(TOP-REAL 2) | x1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | x1 is non empty Relation-like the carrier of ((TOP-REAL 2) | x1) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | x1),REAL:]
the carrier of ((TOP-REAL 2) | x1) is non empty set
[: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | x1),REAL:] is non empty set
lower_bound (proj2 | x1) is V31() real ext-real Element of REAL
(proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1) is non empty V202() V203() V204() Element of bool REAL
lower_bound ((proj2 | x1) .: the carrier of ((TOP-REAL 2) | x1)) is V31() real ext-real Element of REAL
Cl x1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
S-bound (Cl x1) is V31() real ext-real Element of REAL
(TOP-REAL 2) | (Cl x1) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (Cl x1) is non empty Relation-like the carrier of ((TOP-REAL 2) | (Cl x1)) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:]
the carrier of ((TOP-REAL 2) | (Cl x1)) is non empty set
[: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:] is non empty complex-yielding V193() V194() set
bool [: the carrier of ((TOP-REAL 2) | (Cl x1)),REAL:] is non empty set
lower_bound (proj2 | (Cl x1)) is V31() real ext-real Element of REAL
(proj2 | (Cl x1)) .: the carrier of ((TOP-REAL 2) | (Cl x1)) is non empty V202() V203() V204() Element of bool REAL
lower_bound ((proj2 | (Cl x1)) .: the carrier of ((TOP-REAL 2) | (Cl x1))) is V31() real ext-real Element of REAL
proj2 .: (Cl x1) is non empty V202() V203() V204() Element of bool REAL
proj2 .: x1 is non empty V202() V203() V204() Element of bool REAL
lower_bound (proj2 .: x1) is V31() real ext-real Element of REAL
Cl (proj2 .: x1) is non empty closed V202() V203() V204() Element of bool REAL
lower_bound (Cl (proj2 .: x1)) is V31() real ext-real Element of REAL
lower_bound (proj2 .: (Cl x1)) is V31() real ext-real Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
TOP-REAL x1 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL x1) is non empty set
bool the carrier of (TOP-REAL x1) is non empty set
x2 is Element of bool the carrier of (TOP-REAL x1)
y1 is Element of bool the carrier of (TOP-REAL x1)
x2 /\ y1 is Element of bool the carrier of (TOP-REAL x1)
x1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
TOP-REAL x1 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL x1) is non empty set
bool the carrier of (TOP-REAL x1) is non empty set
x2 is Element of bool the carrier of (TOP-REAL x1)
y1 is Element of bool the carrier of (TOP-REAL x1)
x2 \ y1 is Element of bool the carrier of (TOP-REAL x1)
x2 /\ y1 is Element of bool the carrier of (TOP-REAL x1)
(x2 \ y1) \/ (x2 /\ y1) is Element of bool the carrier of (TOP-REAL x1)
y1 \ y1 is Element of bool the carrier of (TOP-REAL x1)
x2 \ (y1 \ y1) is Element of bool the carrier of (TOP-REAL x1)
x2 \ {} is Element of bool the carrier of (TOP-REAL x1)
x1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
TOP-REAL x1 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL x1) is non empty set
Euclid x1 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL x1 is non empty functional FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = x1 } is set
Pitag_dist x1 is non empty Relation-like [:(REAL x1),(REAL x1):] -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:[:(REAL x1),(REAL x1):],REAL:]
[:(REAL x1),(REAL x1):] is non empty set
[:[:(REAL x1),(REAL x1):],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:(REAL x1),(REAL x1):],REAL:] is non empty set
MetrStruct(# (REAL x1),(Pitag_dist x1) #) is strict MetrStruct
the carrier of (Euclid x1) is non empty set
x2 is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL x1)
y1 is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL x1)
y2 is Element of the carrier of (Euclid x1)
a is Element of the carrier of (Euclid x1)
dist (y2,a) is V31() real ext-real Element of REAL
b is Element of the carrier of (Euclid x1)
O is Element of the carrier of (Euclid x1)
y2 is V31() real ext-real Element of REAL
dist (b,O) is V31() real ext-real Element of REAL
g is Element of the carrier of (Euclid x1)
g is Element of the carrier of (Euclid x1)
a is V31() real ext-real Element of REAL
dist (g,g) is V31() real ext-real Element of REAL
O is Element of the carrier of (Euclid x1)
a is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL x1)
g is Element of the carrier of (Euclid x1)
b is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL x1)
y2 is V31() real ext-real Element of REAL
dist (O,g) is V31() real ext-real Element of REAL
x1 is V31() real ext-real set
x2 is V31() real ext-real set
|[x1,x2]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 is V31() real ext-real set
x1 - y1 is V31() real ext-real set
(x1 - y1) ^2 is V31() real ext-real set
(x1 - y1) * (x1 - y1) is V31() real ext-real set
y2 is V31() real ext-real set
|[y1,y2]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x2 - y2 is V31() real ext-real set
(x2 - y2) ^2 is V31() real ext-real set
(x2 - y2) * (x2 - y2) is V31() real ext-real set
((x1 - y1) ^2) + ((x2 - y2) ^2) is V31() real ext-real set
sqrt (((x1 - y1) ^2) + ((x2 - y2) ^2)) is V31() real ext-real set
a is Element of the carrier of (Euclid 2)
b is Element of the carrier of (Euclid 2)
dist (a,b) is V31() real ext-real Element of REAL
|[x1,x2]| `1 is V31() real ext-real Element of REAL
|[x1,x2]| . 1 is V31() real ext-real Element of REAL
|[y1,y2]| `2 is V31() real ext-real Element of REAL
|[y1,y2]| . 2 is V31() real ext-real Element of REAL
|[y1,y2]| `1 is V31() real ext-real Element of REAL
|[y1,y2]| . 1 is V31() real ext-real Element of REAL
|[x1,x2]| `2 is V31() real ext-real Element of REAL
|[x1,x2]| . 2 is V31() real ext-real Element of REAL
(Pitag_dist 2) . (a,b) is set
[a,b] is set
{a,b} is non empty finite set
{a} is non empty finite set
{{a,b},{a}} is non empty finite V40() set
(Pitag_dist 2) . [a,b] is V31() real ext-real set
x1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
x1 `1 is V31() real ext-real Element of REAL
x1 . 1 is V31() real ext-real Element of REAL
x1 `2 is V31() real ext-real Element of REAL
x1 . 2 is V31() real ext-real Element of REAL
x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
(2,x1,x2) is V31() real ext-real Element of REAL
x2 `1 is V31() real ext-real Element of REAL
x2 . 1 is V31() real ext-real Element of REAL
(x1 `1) - (x2 `1) is V31() real ext-real Element of REAL
((x1 `1) - (x2 `1)) ^2 is V31() real ext-real Element of REAL
((x1 `1) - (x2 `1)) * ((x1 `1) - (x2 `1)) is V31() real ext-real set
x2 `2 is V31() real ext-real Element of REAL
x2 . 2 is V31() real ext-real Element of REAL
(x1 `2) - (x2 `2) is V31() real ext-real Element of REAL
((x1 `2) - (x2 `2)) ^2 is V31() real ext-real Element of REAL
((x1 `2) - (x2 `2)) * ((x1 `2) - (x2 `2)) is V31() real ext-real set
(((x1 `1) - (x2 `1)) ^2) + (((x1 `2) - (x2 `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((x1 `1) - (x2 `1)) ^2) + (((x1 `2) - (x2 `2)) ^2)) is V31() real ext-real Element of REAL
|[(x1 `1),(x1 `2)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
|[(x2 `1),(x2 `2)]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
y1 is Element of the carrier of (Euclid 2)
y2 is Element of the carrier of (Euclid 2)
dist (y1,y2) is V31() real ext-real Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
TOP-REAL x1 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL x1) is non empty set
x2 is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL x1)
(x1,x2,x2) is V31() real ext-real Element of REAL
Euclid x1 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL x1 is non empty functional FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = x1 } is set
Pitag_dist x1 is non empty Relation-like [:(REAL x1),(REAL x1):] -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:[:(REAL x1),(REAL x1):],REAL:]
[:(REAL x1),(REAL x1):] is non empty set
[:[:(REAL x1),(REAL x1):],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:(REAL x1),(REAL x1):],REAL:] is non empty set
MetrStruct(# (REAL x1),(Pitag_dist x1) #) is strict MetrStruct
the carrier of (Euclid x1) is non empty set
y1 is Element of the carrier of (Euclid x1)
y2 is Element of the carrier of (Euclid x1)
dist (y1,y2) is V31() real ext-real Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT
TOP-REAL x1 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL x1) is non empty set
x2 is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL x1)
y2 is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL x1)
(x1,x2,y2) is V31() real ext-real Element of REAL
y1 is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL x1)
(x1,x2,y1) is V31() real ext-real Element of REAL
(x1,y1,y2) is V31() real ext-real Element of REAL
(x1,x2,y1) + (x1,y1,y2) is V31() real ext-real Element of REAL
Euclid x1 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL x1 is non empty functional FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = x1 } is set
Pitag_dist x1 is non empty Relation-like [:(REAL x1),(REAL x1):] -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:[:(REAL x1),(REAL x1):],REAL:]
[:(REAL x1),(REAL x1):] is non empty set
[:[:(REAL x1),(REAL x1):],REAL:] is non empty complex-yielding V193() V194() set
bool [:[:(REAL x1),(REAL x1):],REAL:] is non empty set
MetrStruct(# (REAL x1),(Pitag_dist x1) #) is strict MetrStruct
the carrier of (Euclid x1) is non empty set
a is Element of the carrier of (Euclid x1)
b is Element of the carrier of (Euclid x1)
dist (a,b) is V31() real ext-real Element of REAL
O is Element of the carrier of (Euclid x1)
g is Element of the carrier of (Euclid x1)
dist (O,g) is V31() real ext-real Element of REAL
g is Element of the carrier of (Euclid x1)
B is Element of the carrier of (Euclid x1)
dist (g,B) is V31() real ext-real Element of REAL
x1 is V31() real ext-real set
x2 is V31() real ext-real set
y1 is V31() real ext-real set
y2 is V31() real ext-real set
x2 - x1 is V31() real ext-real set
y2 - y1 is V31() real ext-real set
(x2 - x1) + (y2 - y1) is V31() real ext-real set
a is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
a `1 is V31() real ext-real Element of REAL
a . 1 is V31() real ext-real Element of REAL
a `2 is V31() real ext-real Element of REAL
a . 2 is V31() real ext-real Element of REAL
b is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)
b `1 is V31() real ext-real Element of REAL
b . 1 is V31() real ext-real Element of REAL
b `2 is V31() real ext-real Element of REAL
b . 2 is V31() real ext-real Element of REAL
(2,a,b) is V31() real ext-real Element of REAL
(a `2) - (b `2) is V31() real ext-real Element of REAL
abs ((a `2) - (b `2)) is V31() real ext-real Element of REAL
(a `1) - (b `1) is V31() real ext-real Element of REAL
((a `1) - (b `1)) ^2 is V31() real ext-real Element of REAL
((a `1) - (b `1)) * ((a `1) - (b `1)) is V31() real ext-real set
((a `2) - (b `2)) ^2 is V31() real ext-real Element of REAL
((a `2) - (b `2)) * ((a `2) - (b `2)) is V31() real ext-real set
(((a `1) - (b `1)) ^2) + (((a `2) - (b `2)) ^2) is V31() real ext-real Element of REAL
sqrt ((((a `1) - (b `1)) ^2) + (((a `2) - (b `2)) ^2)) is V31() real ext-real Element of REAL
sqrt (((a `1) - (b `1)) ^2) is V31() real ext-real Element of REAL
sqrt (((a `2) - (b `2)) ^2) is V31() real ext-real Element of REAL
(sqrt (((a `1) - (b `1)) ^2)) + (sqrt (((a `2) - (b `2)) ^2)) is V31() real ext-real Element of REAL
abs ((a `1) - (b `1)) is V31() real ext-real Element of REAL
(abs ((a `1) - (b `1))) + (sqrt (((a `2) - (b `2)) ^2)) is V31() real ext-real Element of REAL
(abs ((a `1) - (b `1))) + (abs ((a `2) - (b `2))) is V31() real ext-real Element of REAL