REAL is V163() V164() V165() V169() set
NAT is V163() V164() V165() V166() V167() V168() V169() Element of K6(REAL)
K6(REAL) is non empty set
COMPLEX is V163() V169() set
omega is V163() V164() V165() V166() V167() V168() V169() set
K6(omega) is non empty set
I[01] is non empty strict TopSpace-like TopStruct
the carrier of I[01] is non empty set
1 is non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() Element of NAT
K7(1,1) is non empty set
K6(K7(1,1)) is non empty set
K7(K7(1,1),1) is non empty set
K6(K7(K7(1,1),1)) is non empty set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is non empty set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
2 is non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() Element of NAT
K7(2,2) is non empty set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is non empty set
RealSpace is strict MetrStruct
K263() is TopSpace-like TopStruct
K6(NAT) is non empty set
RAT is V163() V164() V165() V166() V169() set
INT is V163() V164() V165() V166() V167() V169() set
K6(K7(REAL,REAL)) is non empty set
TOP-REAL 2 is non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K6( the carrier of (TOP-REAL 2)) is non empty set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is non empty set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is non empty set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is non empty set
K7(INT,INT) is set
K6(K7(INT,INT)) is non empty set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is non empty set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is non empty set
{} is empty V163() V164() V165() V166() V167() V168() V169() set
the empty V163() V164() V165() V166() V167() V168() V169() set is empty V163() V164() V165() V166() V167() V168() V169() set
0 is empty natural V11() real ext-real V115() V116() V163() V164() V165() V166() V167() V168() V169() Element of NAT
[.0,1.] is V163() V164() V165() Element of K6(REAL)
K265() is non empty strict TopSpace-like SubSpace of K263()
the carrier of K265() is non empty set
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
REAL 2 is non empty V114() M18( REAL )
K383(2,REAL) is V114() M18( REAL )
Pitag_dist 2 is V22() V25(K7((REAL 2),(REAL 2))) V26( REAL ) Function-like V33(K7((REAL 2),(REAL 2)), REAL ) Element of K6(K7(K7((REAL 2),(REAL 2)),REAL))
K7((REAL 2),(REAL 2)) is non empty set
K7(K7((REAL 2),(REAL 2)),REAL) is set
K6(K7(K7((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
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p is non empty TopSpace-like TopStruct
the carrier of p is non empty set
K7( the carrier of I[01], the carrier of p) is non empty set
K6(K7( the carrier of I[01], the carrier of p)) is non empty set
y0 is Element of the carrier of p
P is Element of the carrier of p
w1 is V22() V25( the carrier of I[01]) V26( the carrier of p) Function-like V33( the carrier of I[01], the carrier of p) Element of K6(K7( the carrier of I[01], the carrier of p))
w1 . 0 is set
w1 . 1 is set
dom w1 is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is non empty set
rng w1 is Element of K6( the carrier of p)
K6( the carrier of p) is non empty set
w1 is non empty TopSpace-like TopStruct
the carrier of w1 is non empty set
K7( the carrier of w1, the carrier of p) is non empty set
K6(K7( the carrier of w1, the carrier of p)) is non empty set
w2 is V22() V25( the carrier of w1) V26( the carrier of p) Function-like V33( the carrier of w1, the carrier of p) Element of K6(K7( the carrier of w1, the carrier of p))
rng w2 is Element of K6( the carrier of p)
p is non empty TopSpace-like TopStruct
the carrier of p is non empty set
K6( the carrier of p) is non empty set
y0 is Element of K6( the carrier of p)
p | y0 is strict TopSpace-like SubSpace of p
the carrier of (p | y0) is set
K7( the carrier of I[01], the carrier of (p | y0)) is set
K6(K7( the carrier of I[01], the carrier of (p | y0))) is non empty set
P is non empty Element of K6( the carrier of p)
p | P is non empty strict TopSpace-like SubSpace of p
the carrier of (p | P) is non empty set
K7( the carrier of I[01], the carrier of (p | P)) is non empty set
K6(K7( the carrier of I[01], the carrier of (p | P))) is non empty set
w1 is Element of the carrier of p
w2 is Element of the carrier of p
x1 is Element of the carrier of (p | P)
I[01] --> x1 is V22() V25( the carrier of I[01]) V26( the carrier of (p | P)) Function-like V33( the carrier of I[01], the carrier of (p | P)) continuous Element of K6(K7( the carrier of I[01], the carrier of (p | P)))
K431( the carrier of (p | P), the carrier of I[01],x1) is V22() V25( the carrier of I[01]) V26( the carrier of (p | P)) Function-like V33( the carrier of I[01], the carrier of (p | P)) Element of K6(K7( the carrier of I[01], the carrier of (p | P)))
x2 is V22() V25( the carrier of I[01]) V26( the carrier of (p | P)) Function-like V33( the carrier of I[01], the carrier of (p | P)) Element of K6(K7( the carrier of I[01], the carrier of (p | P)))
x2 . 0 is set
x2 . 1 is set
w1 is Element of the carrier of (p | P)
w2 is Element of the carrier of (p | P)
[#] (p | P) is non empty non proper closed Element of K6( the carrier of (p | P))
K6( the carrier of (p | P)) is non empty set
K6( the carrier of (p | y0)) is non empty set
[#] (p | y0) is non proper closed Element of K6( the carrier of (p | y0))
w1 is Element of K6( the carrier of (p | y0))
w2 is Element of K6( the carrier of (p | y0))
w1 \/ w2 is Element of K6( the carrier of (p | y0))
{} (p | y0) is empty closed V163() V164() V165() V166() V167() V168() V169() Element of K6( the carrier of (p | y0))
P is empty proper closed V163() V164() V165() V166() V167() V168() V169() Element of K6( the carrier of p)
p | P is empty V50() V51() {} -element strict TopSpace-like T_0 SubSpace of p
[#] (p | P) is empty V2() non proper closed V163() V164() V165() V166() V167() V168() V169() Element of K6( the carrier of (p | P))
the carrier of (p | P) is empty V2() V36() V163() V164() V165() V166() V167() V168() V169() set
K6( the carrier of (p | P)) is non empty set
p is non empty TopSpace-like TopStruct
the carrier of p is non empty set
K6( the carrier of p) is non empty set
y0 is Element of K6( the carrier of p)
P is Element of K6( the carrier of p)
y0 \/ P is Element of K6( the carrier of p)
p is non empty TopSpace-like TopStruct
the carrier of p is non empty set
K6( the carrier of p) is non empty set
y0 is Element of K6( the carrier of p)
P is Element of K6( the carrier of p)
w1 is Element of K6( the carrier of p)
y0 \/ P is Element of K6( the carrier of p)
(y0 \/ P) \/ w1 is Element of K6( the carrier of p)
P /\ w1 is Element of K6( the carrier of p)
(y0 \/ P) /\ w1 is Element of K6( the carrier of p)
y0 /\ w1 is Element of K6( the carrier of p)
(y0 /\ w1) \/ (P /\ w1) is Element of K6( the carrier of p)
p is non empty TopSpace-like TopStruct
the carrier of p is non empty set
K6( the carrier of p) is non empty set
y0 is Element of K6( the carrier of p)
P is Element of K6( the carrier of p)
w1 is Element of K6( the carrier of p)
w2 is Element of K6( the carrier of p)
y0 \/ P is Element of K6( the carrier of p)
(y0 \/ P) \/ w1 is Element of K6( the carrier of p)
((y0 \/ P) \/ w1) \/ w2 is Element of K6( the carrier of p)
w1 /\ w2 is Element of K6( the carrier of p)
((y0 \/ P) \/ w1) /\ w2 is Element of K6( the carrier of p)
(y0 \/ P) /\ w2 is Element of K6( the carrier of p)
((y0 \/ P) /\ w2) \/ (w1 /\ w2) is Element of K6( the carrier of p)
p is non empty V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of p is non empty set
K6( the carrier of p) is non empty set
y0 is Element of K6( the carrier of p)
P is Element of the carrier of p
w1 is Element of the carrier of p
LSeg (P,w1) is non empty convex Element of K6( the carrier of p)
{ (((1 - b1) * P) + (b1 * w1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p is natural V11() real ext-real set
TOP-REAL p is non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RLTopStruct
the carrier of (TOP-REAL p) is non empty set
K6( the carrier of (TOP-REAL p)) is non empty set
y0 is Element of K6( the carrier of (TOP-REAL p))
(TOP-REAL p) | y0 is strict TopSpace-like SubSpace of TOP-REAL p
the carrier of ((TOP-REAL p) | y0) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL p) | y0)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL p) | y0))) is non empty set
P is V43(p) V112() V155() Element of the carrier of (TOP-REAL p)
w1 is V43(p) V112() V155() Element of the carrier of (TOP-REAL p)
LSeg (P,w1) is non empty convex Element of K6( the carrier of (TOP-REAL p))
{ (((1 - b1) * P) + (b1 * w1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(TOP-REAL p) | (LSeg (P,w1)) is non empty strict TopSpace-like SubSpace of TOP-REAL p
the carrier of ((TOP-REAL p) | (LSeg (P,w1))) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (P,w1)))) is non empty set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (P,w1))))) is non empty set
w2 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL p) | (LSeg (P,w1)))) Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (P,w1)))) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (P,w1)))))
w2 . 0 is set
w2 . 1 is set
rng w2 is Element of K6( the carrier of ((TOP-REAL p) | (LSeg (P,w1))))
K6( the carrier of ((TOP-REAL p) | (LSeg (P,w1)))) is non empty set
[#] ((TOP-REAL p) | (LSeg (P,w1))) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL p) | (LSeg (P,w1))))
[#] ((TOP-REAL p) | y0) is non proper closed Element of K6( the carrier of ((TOP-REAL p) | y0))
K6( the carrier of ((TOP-REAL p) | y0)) is non empty set
dom w2 is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is non empty set
K7([.0,1.],y0) is set
K6(K7([.0,1.],y0)) is non empty set
x1 is V22() V25([.0,1.]) V26(y0) Function-like V33([.0,1.],y0) Element of K6(K7([.0,1.],y0))
x2 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL p) | y0)) Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL p) | y0)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL p) | y0)))
K6((REAL 2)) is non empty set
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } is set
y0 is set
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
|[P,w1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b2 } is set
y0 is set
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
|[P,w1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= p } is set
y0 is set
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
|[P,w1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= p } is set
y0 is set
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
|[P,w1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not b1 <= p & not y0 <= b1 & not b2 <= P & not w1 <= b2 ) } is set
w2 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= y0 or not P <= b2 or not b2 <= w1 ) } is set
w2 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= p } is set
y0 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b1 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= p } /\ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b1 } is set
P is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= P } is set
( { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= p } /\ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b1 } ) /\ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= P } is set
w1 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not b1 <= p & not y0 <= b1 & not b2 <= P & not w1 <= b2 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not w1 <= b2 } is set
(( { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= p } /\ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b1 } ) /\ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= P } ) /\ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not w1 <= b2 } is set
w2 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w2 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v1 is V11() real ext-real Element of REAL
l is V11() real ext-real Element of REAL
|[v1,l]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v `1 is V11() real ext-real Element of REAL
v `2 is V11() real ext-real Element of REAL
v1 is V11() real ext-real Element of REAL
l is V11() real ext-real Element of REAL
|[v1,l]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v1 is V11() real ext-real Element of REAL
l is V11() real ext-real Element of REAL
|[v1,l]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v1 is V11() real ext-real Element of REAL
l is V11() real ext-real Element of REAL
|[v1,l]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } is set
y0 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= y0 } is set
P is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not P <= b2 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not P <= b2 } is set
( { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not P <= b2 } ) \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= y0 } is set
w1 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= y0 or not P <= b2 or not b2 <= w1 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= w1 } is set
(( { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not P <= b2 } ) \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= y0 } ) \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= w1 } is set
w2 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w2 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v is V11() real ext-real Element of REAL
v1 is V11() real ext-real Element of REAL
|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l is V11() real ext-real Element of REAL
q is V11() real ext-real Element of REAL
|[l,q]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
Q is V11() real ext-real Element of REAL
QQ is V11() real ext-real Element of REAL
|[Q,QQ]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not b1 <= p & not P <= b1 & not b2 <= y0 & not w1 <= b2 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
x1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (x1,x2) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * x1) + (b1 * x2)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
v is set
v1 is V11() real ext-real Element of REAL
l is V11() real ext-real Element of REAL
|[v1,l]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x1 `1 is V11() real ext-real Element of REAL
x1 `2 is V11() real ext-real Element of REAL
q is V11() real ext-real Element of REAL
Q is V11() real ext-real Element of REAL
|[q,Q]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x2 `1 is V11() real ext-real Element of REAL
x2 `2 is V11() real ext-real Element of REAL
QQ is V11() real ext-real Element of REAL
1 - QQ is V11() real ext-real Element of REAL
(1 - QQ) * x1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
QQ * x2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - QQ) * x1) + (QQ * x2) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - QQ) * x1) `1 is V11() real ext-real Element of REAL
(QQ * x2) `1 is V11() real ext-real Element of REAL
(((1 - QQ) * x1) `1) + ((QQ * x2) `1) is V11() real ext-real Element of REAL
((1 - QQ) * x1) `2 is V11() real ext-real Element of REAL
(QQ * x2) `2 is V11() real ext-real Element of REAL
(((1 - QQ) * x1) `2) + ((QQ * x2) `2) is V11() real ext-real Element of REAL
|[((((1 - QQ) * x1) `1) + ((QQ * x2) `1)),((((1 - QQ) * x1) `2) + ((QQ * x2) `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(1 - QQ) * (x1 `1) is V11() real ext-real Element of REAL
(1 - QQ) * (x1 `2) is V11() real ext-real Element of REAL
|[((1 - QQ) * (x1 `1)),((1 - QQ) * (x1 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
QQ * (x2 `1) is V11() real ext-real Element of REAL
QQ * (x2 `2) is V11() real ext-real Element of REAL
|[(QQ * (x2 `1)),(QQ * (x2 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(((1 - QQ) * x1) + (QQ * x2)) `1 is V11() real ext-real Element of REAL
((1 - QQ) * (x1 `1)) + (QQ * (x2 `1)) is V11() real ext-real Element of REAL
(((1 - QQ) * x1) + (QQ * x2)) `2 is V11() real ext-real Element of REAL
((1 - QQ) * (x1 `2)) + (QQ * (x2 `2)) is V11() real ext-real Element of REAL
|[((((1 - QQ) * x1) + (QQ * x2)) `1),((((1 - QQ) * x1) + (QQ * x2)) `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= p } is set
y0 is Element of K6( the carrier of (TOP-REAL 2))
P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (P,w1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * P) + (b1 * w1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
w2 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
v is V11() real ext-real Element of REAL
v1 is V11() real ext-real Element of REAL
|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w1 `1 is V11() real ext-real Element of REAL
l is V11() real ext-real Element of REAL
1 - l is V11() real ext-real Element of REAL
(1 - l) * P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * P) + (l * w1) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * P) `1 is V11() real ext-real Element of REAL
(l * w1) `1 is V11() real ext-real Element of REAL
(((1 - l) * P) `1) + ((l * w1) `1) is V11() real ext-real Element of REAL
((1 - l) * P) `2 is V11() real ext-real Element of REAL
(l * w1) `2 is V11() real ext-real Element of REAL
(((1 - l) * P) `2) + ((l * w1) `2) is V11() real ext-real Element of REAL
|[((((1 - l) * P) `1) + ((l * w1) `1)),((((1 - l) * P) `2) + ((l * w1) `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(1 - l) * (P `1) is V11() real ext-real Element of REAL
P `2 is V11() real ext-real Element of REAL
(1 - l) * (P `2) is V11() real ext-real Element of REAL
|[((1 - l) * (P `1)),((1 - l) * (P `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * (w1 `1) is V11() real ext-real Element of REAL
w1 `2 is V11() real ext-real Element of REAL
l * (w1 `2) is V11() real ext-real Element of REAL
|[(l * (w1 `1)),(l * (w1 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(((1 - l) * P) + (l * w1)) `1 is V11() real ext-real Element of REAL
((1 - l) * (P `1)) + (l * (w1 `1)) is V11() real ext-real Element of REAL
(((1 - l) * P) + (l * w1)) `2 is V11() real ext-real Element of REAL
|[((((1 - l) * P) + (l * w1)) `1),((((1 - l) * P) + (l * w1)) `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } is set
y0 is Element of K6( the carrier of (TOP-REAL 2))
P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (P,w1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * P) + (b1 * w1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
w2 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
v is V11() real ext-real Element of REAL
v1 is V11() real ext-real Element of REAL
|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w1 `1 is V11() real ext-real Element of REAL
l is V11() real ext-real Element of REAL
1 - l is V11() real ext-real Element of REAL
(1 - l) * P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * P) + (l * w1) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * P) `1 is V11() real ext-real Element of REAL
(l * w1) `1 is V11() real ext-real Element of REAL
(((1 - l) * P) `1) + ((l * w1) `1) is V11() real ext-real Element of REAL
((1 - l) * P) `2 is V11() real ext-real Element of REAL
(l * w1) `2 is V11() real ext-real Element of REAL
(((1 - l) * P) `2) + ((l * w1) `2) is V11() real ext-real Element of REAL
|[((((1 - l) * P) `1) + ((l * w1) `1)),((((1 - l) * P) `2) + ((l * w1) `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(1 - l) * (P `1) is V11() real ext-real Element of REAL
P `2 is V11() real ext-real Element of REAL
(1 - l) * (P `2) is V11() real ext-real Element of REAL
|[((1 - l) * (P `1)),((1 - l) * (P `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * (w1 `1) is V11() real ext-real Element of REAL
w1 `2 is V11() real ext-real Element of REAL
l * (w1 `2) is V11() real ext-real Element of REAL
|[(l * (w1 `1)),(l * (w1 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(((1 - l) * P) + (l * w1)) `1 is V11() real ext-real Element of REAL
((1 - l) * (P `1)) + (l * (w1 `1)) is V11() real ext-real Element of REAL
(((1 - l) * P) + (l * w1)) `2 is V11() real ext-real Element of REAL
|[((((1 - l) * P) + (l * w1)) `1),((((1 - l) * P) + (l * w1)) `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= p } is set
y0 is Element of K6( the carrier of (TOP-REAL 2))
P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (P,w1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * P) + (b1 * w1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
w2 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
P `2 is V11() real ext-real Element of REAL
v is V11() real ext-real Element of REAL
v1 is V11() real ext-real Element of REAL
|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w1 `2 is V11() real ext-real Element of REAL
l is V11() real ext-real Element of REAL
1 - l is V11() real ext-real Element of REAL
(1 - l) * P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * P) + (l * w1) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * P) `1 is V11() real ext-real Element of REAL
(l * w1) `1 is V11() real ext-real Element of REAL
(((1 - l) * P) `1) + ((l * w1) `1) is V11() real ext-real Element of REAL
((1 - l) * P) `2 is V11() real ext-real Element of REAL
(l * w1) `2 is V11() real ext-real Element of REAL
(((1 - l) * P) `2) + ((l * w1) `2) is V11() real ext-real Element of REAL
|[((((1 - l) * P) `1) + ((l * w1) `1)),((((1 - l) * P) `2) + ((l * w1) `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
(1 - l) * (P `1) is V11() real ext-real Element of REAL
(1 - l) * (P `2) is V11() real ext-real Element of REAL
|[((1 - l) * (P `1)),((1 - l) * (P `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w1 `1 is V11() real ext-real Element of REAL
l * (w1 `1) is V11() real ext-real Element of REAL
l * (w1 `2) is V11() real ext-real Element of REAL
|[(l * (w1 `1)),(l * (w1 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(((1 - l) * P) + (l * w1)) `2 is V11() real ext-real Element of REAL
((1 - l) * (P `2)) + (l * (w1 `2)) is V11() real ext-real Element of REAL
(((1 - l) * P) + (l * w1)) `1 is V11() real ext-real Element of REAL
|[((((1 - l) * P) + (l * w1)) `1),((((1 - l) * P) + (l * w1)) `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b2 } is set
y0 is Element of K6( the carrier of (TOP-REAL 2))
P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (P,w1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * P) + (b1 * w1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
w2 is set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
P `2 is V11() real ext-real Element of REAL
v is V11() real ext-real Element of REAL
v1 is V11() real ext-real Element of REAL
|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w1 `2 is V11() real ext-real Element of REAL
l is V11() real ext-real Element of REAL
1 - l is V11() real ext-real Element of REAL
(1 - l) * P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * P) + (l * w1) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * P) `1 is V11() real ext-real Element of REAL
(l * w1) `1 is V11() real ext-real Element of REAL
(((1 - l) * P) `1) + ((l * w1) `1) is V11() real ext-real Element of REAL
((1 - l) * P) `2 is V11() real ext-real Element of REAL
(l * w1) `2 is V11() real ext-real Element of REAL
(((1 - l) * P) `2) + ((l * w1) `2) is V11() real ext-real Element of REAL
|[((((1 - l) * P) `1) + ((l * w1) `1)),((((1 - l) * P) `2) + ((l * w1) `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
(1 - l) * (P `1) is V11() real ext-real Element of REAL
(1 - l) * (P `2) is V11() real ext-real Element of REAL
|[((1 - l) * (P `1)),((1 - l) * (P `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w1 `1 is V11() real ext-real Element of REAL
l * (w1 `1) is V11() real ext-real Element of REAL
l * (w1 `2) is V11() real ext-real Element of REAL
|[(l * (w1 `1)),(l * (w1 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(((1 - l) * P) + (l * w1)) `2 is V11() real ext-real Element of REAL
((1 - l) * (P `2)) + (l * (w1 `2)) is V11() real ext-real Element of REAL
(((1 - l) * P) + (l * w1)) `1 is V11() real ext-real Element of REAL
|[((((1 - l) * P) + (l * w1)) `1),((((1 - l) * P) + (l * w1)) `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= P or not y0 <= b2 or not b2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b2 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b2 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= P } is set
( { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b2 } ) \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= P } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= w1 } is set
(( { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b2 } ) \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= P } ) \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= w1 } is set
p - 1 is V11() real ext-real Element of REAL
y0 - 1 is V11() real ext-real Element of REAL
|[(p - 1),(y0 - 1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x1 is Element of K6( the carrier of (TOP-REAL 2))
x2 is Element of K6( the carrier of (TOP-REAL 2))
x1 /\ x2 is Element of K6( the carrier of (TOP-REAL 2))
P + 1 is V11() real ext-real Element of REAL
|[(P + 1),(y0 - 1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v is Element of K6( the carrier of (TOP-REAL 2))
x2 /\ v is Element of K6( the carrier of (TOP-REAL 2))
w1 + 1 is V11() real ext-real Element of REAL
|[(P + 1),(w1 + 1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v1 is Element of K6( the carrier of (TOP-REAL 2))
v /\ v1 is Element of K6( the carrier of (TOP-REAL 2))
the topology of (TOP-REAL 2) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
K6(K6( the carrier of (TOP-REAL 2))) is non empty set
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct
TopSpaceMetr (Euclid 2) is TopStruct
Family_open_set (Euclid 2) is Element of K6(K6( the carrier of (Euclid 2)))
K6( the carrier of (Euclid 2)) is non empty set
K6(K6( the carrier of (Euclid 2))) is non empty set
TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #) is non empty strict TopStruct
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= p } is set
y0 is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
w1 is Element of the carrier of (Euclid 2)
w2 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
|[w2,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w2 - p is V11() real ext-real Element of REAL
(w2 - p) / 2 is V11() real ext-real Element of REAL
Ball (w1,((w2 - p) / 2)) is Element of K6( the carrier of (Euclid 2))
v is set
{ b1 where b1 is Element of the carrier of (Euclid 2) : not (w2 - p) / 2 <= dist (w1,b1) } is set
v1 is Element of the carrier of (Euclid 2)
dist (w1,v1) is V11() real ext-real Element of REAL
(Pitag_dist 2) . (w1,v1) is set
l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l `1 is V11() real ext-real Element of REAL
q is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
q `1 is V11() real ext-real Element of REAL
(l `1) - (q `1) is V11() real ext-real Element of REAL
((l `1) - (q `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (q `1)),((l `1) - (q `1))) is V11() real ext-real set
l `2 is V11() real ext-real Element of REAL
q `2 is V11() real ext-real Element of REAL
(l `2) - (q `2) is V11() real ext-real Element of REAL
((l `2) - (q `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (q `2)),((l `2) - (q `2))) is V11() real ext-real set
(((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)) is V11() real ext-real Element of REAL
0 + 0 is V11() real ext-real Element of REAL
((w2 - p) / 2) ^2 is V11() real ext-real Element of REAL
K37(((w2 - p) / 2),((w2 - p) / 2)) is V11() real ext-real set
(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))),(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)))) is V11() real ext-real set
(q `1) + ((w2 - p) / 2) is V11() real ext-real Element of REAL
(l `1) - ((w2 - p) / 2) is V11() real ext-real Element of REAL
w2 - ((w2 - p) / 2) is V11() real ext-real Element of REAL
((w2 - p) / 2) + p is V11() real ext-real Element of REAL
|[(q `1),(q `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
P is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } is set
y0 is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
w1 is Element of the carrier of (Euclid 2)
w2 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
|[w2,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p - w2 is V11() real ext-real Element of REAL
(p - w2) / 2 is V11() real ext-real Element of REAL
Ball (w1,((p - w2) / 2)) is Element of K6( the carrier of (Euclid 2))
v is set
{ b1 where b1 is Element of the carrier of (Euclid 2) : not (p - w2) / 2 <= dist (w1,b1) } is set
v1 is Element of the carrier of (Euclid 2)
dist (w1,v1) is V11() real ext-real Element of REAL
(Pitag_dist 2) . (w1,v1) is set
l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l `1 is V11() real ext-real Element of REAL
q is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
q `1 is V11() real ext-real Element of REAL
(l `1) - (q `1) is V11() real ext-real Element of REAL
((l `1) - (q `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (q `1)),((l `1) - (q `1))) is V11() real ext-real set
l `2 is V11() real ext-real Element of REAL
q `2 is V11() real ext-real Element of REAL
(l `2) - (q `2) is V11() real ext-real Element of REAL
((l `2) - (q `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (q `2)),((l `2) - (q `2))) is V11() real ext-real set
(((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)) is V11() real ext-real Element of REAL
0 + 0 is V11() real ext-real Element of REAL
((p - w2) / 2) ^2 is V11() real ext-real Element of REAL
K37(((p - w2) / 2),((p - w2) / 2)) is V11() real ext-real set
(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))),(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)))) is V11() real ext-real set
(q `1) - (l `1) is V11() real ext-real Element of REAL
((q `1) - (l `1)) ^2 is V11() real ext-real Element of REAL
K37(((q `1) - (l `1)),((q `1) - (l `1))) is V11() real ext-real set
(l `1) + ((p - w2) / 2) is V11() real ext-real Element of REAL
w2 + ((p - w2) / 2) is V11() real ext-real Element of REAL
p - ((p - w2) / 2) is V11() real ext-real Element of REAL
|[(q `1),(q `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
P is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= p } is set
y0 is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
w1 is Element of the carrier of (Euclid 2)
w2 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
|[w2,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x1 - p is V11() real ext-real Element of REAL
(x1 - p) / 2 is V11() real ext-real Element of REAL
Ball (w1,((x1 - p) / 2)) is Element of K6( the carrier of (Euclid 2))
v is set
{ b1 where b1 is Element of the carrier of (Euclid 2) : not (x1 - p) / 2 <= dist (w1,b1) } is set
v1 is Element of the carrier of (Euclid 2)
dist (w1,v1) is V11() real ext-real Element of REAL
(Pitag_dist 2) . (w1,v1) is set
l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l `1 is V11() real ext-real Element of REAL
q is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
q `1 is V11() real ext-real Element of REAL
(l `1) - (q `1) is V11() real ext-real Element of REAL
((l `1) - (q `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (q `1)),((l `1) - (q `1))) is V11() real ext-real set
l `2 is V11() real ext-real Element of REAL
q `2 is V11() real ext-real Element of REAL
(l `2) - (q `2) is V11() real ext-real Element of REAL
((l `2) - (q `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (q `2)),((l `2) - (q `2))) is V11() real ext-real set
(((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)) is V11() real ext-real Element of REAL
0 + 0 is V11() real ext-real Element of REAL
((x1 - p) / 2) ^2 is V11() real ext-real Element of REAL
K37(((x1 - p) / 2),((x1 - p) / 2)) is V11() real ext-real set
(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))),(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)))) is V11() real ext-real set
(((l `2) - (q `2)) ^2) + (((l `1) - (q `1)) ^2) is V11() real ext-real Element of REAL
(q `2) + ((x1 - p) / 2) is V11() real ext-real Element of REAL
(l `2) - ((x1 - p) / 2) is V11() real ext-real Element of REAL
x1 - ((x1 - p) / 2) is V11() real ext-real Element of REAL
((x1 - p) / 2) + p is V11() real ext-real Element of REAL
|[(q `1),(q `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
P is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
p is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b2 } is set
y0 is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
w1 is Element of the carrier of (Euclid 2)
w2 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
|[w2,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p - x1 is V11() real ext-real Element of REAL
(p - x1) / 2 is V11() real ext-real Element of REAL
Ball (w1,((p - x1) / 2)) is Element of K6( the carrier of (Euclid 2))
v is set
{ b1 where b1 is Element of the carrier of (Euclid 2) : not (p - x1) / 2 <= dist (w1,b1) } is set
v1 is Element of the carrier of (Euclid 2)
dist (w1,v1) is V11() real ext-real Element of REAL
(Pitag_dist 2) . (w1,v1) is set
l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l `1 is V11() real ext-real Element of REAL
q is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
q `1 is V11() real ext-real Element of REAL
(l `1) - (q `1) is V11() real ext-real Element of REAL
((l `1) - (q `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (q `1)),((l `1) - (q `1))) is V11() real ext-real set
l `2 is V11() real ext-real Element of REAL
q `2 is V11() real ext-real Element of REAL
(l `2) - (q `2) is V11() real ext-real Element of REAL
((l `2) - (q `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (q `2)),((l `2) - (q `2))) is V11() real ext-real set
(((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)) is V11() real ext-real Element of REAL
0 + 0 is V11() real ext-real Element of REAL
((p - x1) / 2) ^2 is V11() real ext-real Element of REAL
K37(((p - x1) / 2),((p - x1) / 2)) is V11() real ext-real set
(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))),(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)))) is V11() real ext-real set
(q `2) - (l `2) is V11() real ext-real Element of REAL
((q `2) - (l `2)) ^2 is V11() real ext-real Element of REAL
K37(((q `2) - (l `2)),((q `2) - (l `2))) is V11() real ext-real set
(l `2) + ((p - x1) / 2) is V11() real ext-real Element of REAL
x1 + ((p - x1) / 2) is V11() real ext-real Element of REAL
p - ((p - x1) / 2) is V11() real ext-real Element of REAL
|[(q `1),(q `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
P is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not b1 <= p & not P <= b1 & not b2 <= y0 & not w1 <= b2 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= p } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not P <= b1 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= y0 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not w1 <= b2 } is set
x1 is Element of K6( the carrier of (TOP-REAL 2))
x2 is Element of K6( the carrier of (TOP-REAL 2))
x1 /\ x2 is Element of K6( the carrier of (TOP-REAL 2))
v is Element of K6( the carrier of (TOP-REAL 2))
(x1 /\ x2) /\ v is Element of K6( the carrier of (TOP-REAL 2))
v1 is Element of K6( the carrier of (TOP-REAL 2))
((x1 /\ x2) /\ v) /\ v1 is Element of K6( the carrier of (TOP-REAL 2))
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= P or not y0 <= b2 or not b2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b2 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b2 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= P } is set
( { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b2 } ) \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= P } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= w1 } is set
(( { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b2 } ) \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= P } ) \/ { |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= w1 } is set
x1 is Element of K6( the carrier of (TOP-REAL 2))
x2 is Element of K6( the carrier of (TOP-REAL 2))
x1 \/ x2 is Element of K6( the carrier of (TOP-REAL 2))
v is Element of K6( the carrier of (TOP-REAL 2))
(x1 \/ x2) \/ v is Element of K6( the carrier of (TOP-REAL 2))
v1 is Element of K6( the carrier of (TOP-REAL 2))
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not b1 <= p & not P <= b1 & not b2 <= y0 & not w1 <= b2 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= P or not y0 <= b2 or not b2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
x1 is Element of K6( the carrier of (TOP-REAL 2))
x2 is set
v is V11() real ext-real Element of REAL
v1 is V11() real ext-real Element of REAL
|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[v,v1]| `1 is V11() real ext-real Element of REAL
|[v,v1]| `2 is V11() real ext-real Element of REAL
q is V11() real ext-real Element of REAL
Q is V11() real ext-real Element of REAL
|[q,Q]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not y0 <= b1 `1 & not b1 `2 <= P & not w1 <= b1 `2 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not b1 <= p & not y0 <= b1 & not b2 <= P & not w1 <= b2 ) } is set
w2 is set
x1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x1 `1 is V11() real ext-real Element of REAL
x1 `2 is V11() real ext-real Element of REAL
|[(x1 `1),(x1 `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[x1,x2]| `1 is V11() real ext-real Element of REAL
|[x1,x2]| `2 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= y0 or not P <= b1 `2 or not b1 `2 <= w1 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= y0 or not P <= b2 or not b2 <= w1 ) } is set
w2 is set
x1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x1 `1 is V11() real ext-real Element of REAL
x1 `2 is V11() real ext-real Element of REAL
|[(x1 `1),(x1 `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[x1,x2]| `1 is V11() real ext-real Element of REAL
|[x1,x2]| `2 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not y0 <= b1 `1 & not b1 `2 <= P & not w1 <= b1 `2 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not b1 <= p & not y0 <= b1 & not b2 <= P & not w1 <= b2 ) } is set
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= y0 or not P <= b1 `2 or not b1 `2 <= w1 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= y0 or not P <= b2 or not b2 <= w1 ) } is set
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not P <= b1 `1 & not b1 `2 <= y0 & not w1 <= b1 `2 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not b1 <= p & not P <= b1 & not b2 <= y0 & not w1 <= b2 ) } is set
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= P or not y0 <= b1 `2 or not b1 `2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= P or not y0 <= b2 or not b2 <= w1 ) } is set
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not P <= b1 `1 & not b1 `2 <= y0 & not w1 <= b1 `2 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not b1 <= p & not P <= b1 & not b2 <= y0 & not w1 <= b2 ) } is set
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= P or not y0 <= b1 `2 or not b1 `2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= P or not y0 <= b2 or not b2 <= w1 ) } is set
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not P <= b1 `1 & not b1 `2 <= y0 & not w1 <= b1 `2 ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= P or not y0 <= b1 `2 or not b1 `2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
x1 is Element of K6( the carrier of (TOP-REAL 2))
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not b1 <= p & not P <= b1 & not b2 <= y0 & not w1 <= b2 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= P or not y0 <= b2 or not b2 <= w1 ) } is set
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & y0 <= b1 `2 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = y0 ) or ( b1 `1 = P & b1 `2 <= w1 & y0 <= b1 `2 ) ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not P <= b1 `1 & not b1 `2 <= y0 & not w1 <= b1 `2 ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= P or not y0 <= b1 `2 or not b1 `2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
x1 is Element of K6( the carrier of (TOP-REAL 2))
x2 is Element of K6( the carrier of (TOP-REAL 2))
w2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ w2 is set
x1 \/ x2 is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (w2 `) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (w2 `)) is set
K6( the carrier of ((TOP-REAL 2) | (w2 `))) is non empty set
v is set
v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v1 `1 is V11() real ext-real Element of REAL
v1 `2 is V11() real ext-real Element of REAL
v is set
v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v1 `1 is V11() real ext-real Element of REAL
v1 `2 is V11() real ext-real Element of REAL
l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l `1 is V11() real ext-real Element of REAL
l `2 is V11() real ext-real Element of REAL
v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v1 `1 is V11() real ext-real Element of REAL
v1 `2 is V11() real ext-real Element of REAL
l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l `1 is V11() real ext-real Element of REAL
l `2 is V11() real ext-real Element of REAL
p + P is V11() real ext-real Element of REAL
(p + P) / 2 is V11() real ext-real Element of REAL
y0 + w1 is V11() real ext-real Element of REAL
(y0 + w1) / 2 is V11() real ext-real Element of REAL
p + p is V11() real ext-real Element of REAL
y0 + y0 is V11() real ext-real Element of REAL
(p + p) / 2 is V11() real ext-real Element of REAL
(y0 + y0) / 2 is V11() real ext-real Element of REAL
P + P is V11() real ext-real Element of REAL
w1 + w1 is V11() real ext-real Element of REAL
(P + P) / 2 is V11() real ext-real Element of REAL
(w1 + w1) / 2 is V11() real ext-real Element of REAL
|[((p + P) / 2),((y0 + w1) / 2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((p + P) / 2),((y0 + w1) / 2)]| `1 is V11() real ext-real Element of REAL
|[((p + P) / 2),((y0 + w1) / 2)]| `2 is V11() real ext-real Element of REAL
x1 /\ x2 is Element of K6( the carrier of (TOP-REAL 2))
Q is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
QQ is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( not p <= b1 or not b1 <= P or not y0 <= b2 or not b2 <= w1 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not p <= b1 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not y0 <= b2 } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b1 <= P } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : not b2 <= w1 } is set
r is Element of K6( the carrier of (TOP-REAL 2))
r is Element of K6( the carrier of (TOP-REAL 2))
r \/ r is Element of K6( the carrier of (TOP-REAL 2))
pa is Element of K6( the carrier of (TOP-REAL 2))
(r \/ r) \/ pa is Element of K6( the carrier of (TOP-REAL 2))
qa is Element of K6( the carrier of (TOP-REAL 2))
((r \/ r) \/ pa) \/ qa is Element of K6( the carrier of (TOP-REAL 2))
w1 + 1 is V11() real ext-real Element of REAL
P + 1 is V11() real ext-real Element of REAL
|[(P + 1),(w1 + 1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
((TOP-REAL 2) | (w2 `)) | qa is strict TopSpace-like SubSpace of (TOP-REAL 2) | (w2 `)
Q /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
the carrier of (((TOP-REAL 2) | (w2 `)) | qa) is set
K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa)) is non empty set
x1 /\ (w2 `) is Element of K6( the carrier of (TOP-REAL 2))
[#] ((TOP-REAL 2) | (w2 `)) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
x1 /\ ([#] ((TOP-REAL 2) | (w2 `))) is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
the topology of ((TOP-REAL 2) | (w2 `)) is non empty Element of K6(K6( the carrier of ((TOP-REAL 2) | (w2 `))))
K6(K6( the carrier of ((TOP-REAL 2) | (w2 `)))) is non empty set
[#] (((TOP-REAL 2) | (w2 `)) | qa) is non proper closed Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
BP is Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
{} (((TOP-REAL 2) | (w2 `)) | qa) is empty closed V163() V164() V165() V166() V167() V168() V169() Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
the topology of (((TOP-REAL 2) | (w2 `)) | qa) is non empty Element of K6(K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa)))
K6(K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))) is non empty set
QQ /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
x2 /\ (w2 `) is Element of K6( the carrier of (TOP-REAL 2))
x2 /\ ([#] ((TOP-REAL 2) | (w2 `))) is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
AP is Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
Q \/ QQ is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
(Q \/ QQ) /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
BP \/ AP is Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
BP /\ AP is Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
Q /\ (QQ /\ qa) is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
(Q /\ (QQ /\ qa)) /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
Q /\ QQ is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
(Q /\ QQ) /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
((Q /\ QQ) /\ qa) /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
qa /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
(Q /\ QQ) /\ (qa /\ qa) is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
((TOP-REAL 2) | (w2 `)) | qa is strict TopSpace-like SubSpace of (TOP-REAL 2) | (w2 `)
QQ /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
the carrier of (((TOP-REAL 2) | (w2 `)) | qa) is set
K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa)) is non empty set
x2 /\ (w2 `) is Element of K6( the carrier of (TOP-REAL 2))
[#] ((TOP-REAL 2) | (w2 `)) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
x2 /\ ([#] ((TOP-REAL 2) | (w2 `))) is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
the topology of ((TOP-REAL 2) | (w2 `)) is non empty Element of K6(K6( the carrier of ((TOP-REAL 2) | (w2 `))))
K6(K6( the carrier of ((TOP-REAL 2) | (w2 `)))) is non empty set
[#] (((TOP-REAL 2) | (w2 `)) | qa) is non proper closed Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
BP is Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
{} (((TOP-REAL 2) | (w2 `)) | qa) is empty closed V163() V164() V165() V166() V167() V168() V169() Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
the topology of (((TOP-REAL 2) | (w2 `)) | qa) is non empty Element of K6(K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa)))
K6(K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))) is non empty set
Q /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
x1 /\ (w2 `) is Element of K6( the carrier of (TOP-REAL 2))
x1 /\ ([#] ((TOP-REAL 2) | (w2 `))) is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
AP is Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
Q \/ QQ is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
(Q \/ QQ) /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
AP \/ BP is Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
AP /\ BP is Element of K6( the carrier of (((TOP-REAL 2) | (w2 `)) | qa))
Q /\ (QQ /\ qa) is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
(Q /\ (QQ /\ qa)) /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
Q /\ QQ is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
(Q /\ QQ) /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
((Q /\ QQ) /\ qa) /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
qa /\ qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
(Q /\ QQ) /\ (qa /\ qa) is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
Q is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
QQ is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & y0 <= b1 `2 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = y0 ) or ( b1 `1 = P & b1 `2 <= w1 & y0 <= b1 `2 ) ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not P <= b1 `1 & not b1 `2 <= y0 & not w1 <= b1 `2 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
x1 is Element of K6( the carrier of (TOP-REAL 2))
Cl x1 is Element of K6( the carrier of (TOP-REAL 2))
w2 \/ x1 is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= P or not y0 <= b1 `2 or not b1 `2 <= w1 ) } is set
w2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ w2 is set
v is Element of K6( the carrier of (TOP-REAL 2))
x2 is Element of K6( the carrier of (TOP-REAL 2))
x1 \/ x2 is Element of K6( the carrier of (TOP-REAL 2))
x2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ x2 is set
(x1 \/ x2) ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (x1 \/ x2) is set
[#] (TOP-REAL 2) is non empty non proper closed Element of K6( the carrier of (TOP-REAL 2))
([#] (TOP-REAL 2)) \ x1 is Element of K6( the carrier of (TOP-REAL 2))
([#] (TOP-REAL 2)) \ x2 is Element of K6( the carrier of (TOP-REAL 2))
(([#] (TOP-REAL 2)) \ x1) /\ (([#] (TOP-REAL 2)) \ x2) is Element of K6( the carrier of (TOP-REAL 2))
w2 \/ (x1 \/ x2) is Element of K6( the carrier of (TOP-REAL 2))
(w2 \/ x1) \/ x2 is Element of K6( the carrier of (TOP-REAL 2))
v1 is set
v1 is set
([#] (TOP-REAL 2)) \ (x2 `) is Element of K6( the carrier of (TOP-REAL 2))
(x2 `) ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (x2 `) is set
v1 is set
v1 is set
l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l `1 is V11() real ext-real Element of REAL
l `2 is V11() real ext-real Element of REAL
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1 is V11() real ext-real Element of REAL
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2 is V11() real ext-real Element of REAL
P - (l `1) is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)),((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)),((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2) is V11() real ext-real Element of REAL
(|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1) - (l `1) is V11() real ext-real Element of REAL
((|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1) - (l `1)) ^2 is V11() real ext-real Element of REAL
K37(((|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1) - (l `1)),((|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1) - (l `1))) is V11() real ext-real set
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
(l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1 is V11() real ext-real Element of REAL
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2 is V11() real ext-real Element of REAL
P - (l `1) is V11() real ext-real Element of REAL
w1 - (l `2) is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)),((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)),((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2) is V11() real ext-real Element of REAL
(|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) - (l `1) is V11() real ext-real Element of REAL
((|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) - (l `1)) ^2 is V11() real ext-real Element of REAL
K37(((|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) - (l `1)),((|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) - (l `1))) is V11() real ext-real set
(r / 2) ^2 is V11() real ext-real Element of REAL
K37((r / 2),(r / 2)) is V11() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
2 * (r / 2) is V11() real ext-real Element of REAL
(2 * (r / 2)) * (r / 2) is V11() real ext-real Element of REAL
(((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
(l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1 is V11() real ext-real Element of REAL
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2 is V11() real ext-real Element of REAL
P - (l `1) is V11() real ext-real Element of REAL
(l `2) - y0 is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)),((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)),((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2) is V11() real ext-real Element of REAL
(min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) ^2 is V11() real ext-real Element of REAL
K37((min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))),(min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))) is V11() real ext-real set
(r / 2) ^2 is V11() real ext-real Element of REAL
K37((r / 2),(r / 2)) is V11() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
2 * (r / 2) is V11() real ext-real Element of REAL
(2 * (r / 2)) * (r / 2) is V11() real ext-real Element of REAL
(((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1 is V11() real ext-real Element of REAL
|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2 is V11() real ext-real Element of REAL
(l `2) - y0 is V11() real ext-real Element of REAL
(l `1) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)),((l `1) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1))) is V11() real ext-real set
(l `2) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)),((l `2) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
sqrt ((((l `1) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))),(sqrt ((((l `1) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
(l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1 is V11() real ext-real Element of REAL
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2 is V11() real ext-real Element of REAL
(l `2) - y0 is V11() real ext-real Element of REAL
P - (l `1) is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)),((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)),((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2) is V11() real ext-real Element of REAL
(r / 2) ^2 is V11() real ext-real Element of REAL
K37((r / 2),(r / 2)) is V11() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
2 * (r / 2) is V11() real ext-real Element of REAL
(2 * (r / 2)) * (r / 2) is V11() real ext-real Element of REAL
(((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
(l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1 is V11() real ext-real Element of REAL
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2 is V11() real ext-real Element of REAL
(l `1) - p is V11() real ext-real Element of REAL
(l `2) - y0 is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)),((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)),((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2) is V11() real ext-real Element of REAL
(min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) ^2 is V11() real ext-real Element of REAL
K37((min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))),(min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))) is V11() real ext-real set
(r / 2) ^2 is V11() real ext-real Element of REAL
K37((r / 2),(r / 2)) is V11() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
2 * (r / 2) is V11() real ext-real Element of REAL
(2 * (r / 2)) * (r / 2) is V11() real ext-real Element of REAL
(((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2 is V11() real ext-real Element of REAL
|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1 is V11() real ext-real Element of REAL
w1 - (l `2) is V11() real ext-real Element of REAL
(l `1) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)),((l `1) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1))) is V11() real ext-real set
(l `2) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)),((l `2) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2) is V11() real ext-real Element of REAL
(|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) - (l `2) is V11() real ext-real Element of REAL
((|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) - (l `2)) ^2 is V11() real ext-real Element of REAL
K37(((|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) - (l `2)),((|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) - (l `2))) is V11() real ext-real set
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
sqrt ((((l `1) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))),(sqrt ((((l `1) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
(l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1 is V11() real ext-real Element of REAL
|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2 is V11() real ext-real Element of REAL
P - (l `1) is V11() real ext-real Element of REAL
w1 - (l `2) is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)),((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)),((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2) is V11() real ext-real Element of REAL
(|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) - (l `1) is V11() real ext-real Element of REAL
((|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) - (l `1)) ^2 is V11() real ext-real Element of REAL
K37(((|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) - (l `1)),((|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) - (l `1))) is V11() real ext-real set
(r / 2) ^2 is V11() real ext-real Element of REAL
K37((r / 2),(r / 2)) is V11() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
2 * (r / 2) is V11() real ext-real Element of REAL
(2 * (r / 2)) * (r / 2) is V11() real ext-real Element of REAL
(((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
(l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1 is V11() real ext-real Element of REAL
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2 is V11() real ext-real Element of REAL
w1 - (l `2) is V11() real ext-real Element of REAL
(l `1) - p is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)),((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)),((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2) is V11() real ext-real Element of REAL
(min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) ^2 is V11() real ext-real Element of REAL
K37((min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))),(min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))) is V11() real ext-real set
(r / 2) ^2 is V11() real ext-real Element of REAL
K37((r / 2),(r / 2)) is V11() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
2 * (r / 2) is V11() real ext-real Element of REAL
(2 * (r / 2)) * (r / 2) is V11() real ext-real Element of REAL
(((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2 is V11() real ext-real Element of REAL
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1 is V11() real ext-real Element of REAL
(l `1) - p is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)),((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)),((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),(l `2)]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
(l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2 is V11() real ext-real Element of REAL
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1 is V11() real ext-real Element of REAL
(l `1) - p is V11() real ext-real Element of REAL
w1 - (l `2) is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)),((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)),((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2) is V11() real ext-real Element of REAL
(r / 2) ^2 is V11() real ext-real Element of REAL
K37((r / 2),(r / 2)) is V11() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
2 * (r / 2) is V11() real ext-real Element of REAL
(2 * (r / 2)) * (r / 2) is V11() real ext-real Element of REAL
(((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) + (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
(P - p) / 2 is V11() real ext-real Element of REAL
w1 - y0 is V11() real ext-real Element of REAL
(w1 - y0) / 2 is V11() real ext-real Element of REAL
min (((P - p) / 2),((w1 - y0) / 2)) is V11() real ext-real Element of REAL
min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))) is V11() real ext-real Element of REAL
(l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
(l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) is V11() real ext-real Element of REAL
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1 is V11() real ext-real Element of REAL
|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2 is V11() real ext-real Element of REAL
(l `1) - p is V11() real ext-real Element of REAL
(l `2) - y0 is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)),((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)),((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2) is V11() real ext-real Element of REAL
(min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))) ^2 is V11() real ext-real Element of REAL
K37((min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))),(min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))) is V11() real ext-real set
(r / 2) ^2 is V11() real ext-real Element of REAL
K37((r / 2),(r / 2)) is V11() real ext-real set
((r / 2) ^2) + ((r / 2) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
2 * (r / 2) is V11() real ext-real Element of REAL
(2 * (r / 2)) * (r / 2) is V11() real ext-real Element of REAL
(((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) is V11() real ext-real Element of REAL
sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `1)) ^2) + (((l `2) - (|[((l `1) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2)))))),((l `2) - (min ((r / 2),(min (((P - p) / 2),((w1 - y0) / 2))))))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & y0 <= b1 `2 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = y0 ) or ( b1 `1 = P & b1 `2 <= w1 & y0 <= b1 `2 ) ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= P or not y0 <= b1 `2 or not b1 `2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
x1 is Element of K6( the carrier of (TOP-REAL 2))
Cl x1 is Element of K6( the carrier of (TOP-REAL 2))
w2 \/ x1 is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not P <= b1 `1 & not b1 `2 <= y0 & not w1 <= b1 `2 ) } is set
w2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ w2 is set
v is Element of K6( the carrier of (TOP-REAL 2))
x2 is Element of K6( the carrier of (TOP-REAL 2))
x2 \/ x1 is Element of K6( the carrier of (TOP-REAL 2))
x2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ x2 is set
(x2 \/ x1) ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (x2 \/ x1) is set
[#] (TOP-REAL 2) is non empty non proper closed Element of K6( the carrier of (TOP-REAL 2))
([#] (TOP-REAL 2)) \ x2 is Element of K6( the carrier of (TOP-REAL 2))
([#] (TOP-REAL 2)) \ x1 is Element of K6( the carrier of (TOP-REAL 2))
(([#] (TOP-REAL 2)) \ x2) /\ (([#] (TOP-REAL 2)) \ x1) is Element of K6( the carrier of (TOP-REAL 2))
x1 \/ x2 is Element of K6( the carrier of (TOP-REAL 2))
w2 \/ (x1 \/ x2) is Element of K6( the carrier of (TOP-REAL 2))
(w2 \/ x1) \/ x2 is Element of K6( the carrier of (TOP-REAL 2))
v1 is set
v1 is set
([#] (TOP-REAL 2)) \ (x2 `) is Element of K6( the carrier of (TOP-REAL 2))
(x2 `) ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (x2 `) is set
v1 is set
v1 is set
l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l `1 is V11() real ext-real Element of REAL
l `2 is V11() real ext-real Element of REAL
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
(l `1) - (r / 2) is V11() real ext-real Element of REAL
|[((l `1) - (r / 2)),(l `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) - (r / 2)),(l `2)]| `1 is V11() real ext-real Element of REAL
|[((l `1) - (r / 2)),(l `2)]| `2 is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) - (r / 2)),(l `2)]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) - (r / 2)),(l `2)]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) - (r / 2)),(l `2)]| `1)),((l `1) - (|[((l `1) - (r / 2)),(l `2)]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) - (r / 2)),(l `2)]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) - (r / 2)),(l `2)]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) - (r / 2)),(l `2)]| `2)),((l `2) - (|[((l `1) - (r / 2)),(l `2)]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) - (r / 2)),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) - (r / 2)),(l `2)]| `2)) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
sqrt ((((l `1) - (|[((l `1) - (r / 2)),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) - (r / 2)),(l `2)]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) - (r / 2)),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) - (r / 2)),(l `2)]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) - (r / 2)),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) - (r / 2)),(l `2)]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) - (r / 2)),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) - (r / 2)),(l `2)]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
x1 /\ Q is Element of K6( the carrier of (TOP-REAL 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
(l `2) + (r / 2) is V11() real ext-real Element of REAL
|[(l `1),((l `2) + (r / 2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[(l `1),((l `2) + (r / 2))]| `1 is V11() real ext-real Element of REAL
|[(l `1),((l `2) + (r / 2))]| `2 is V11() real ext-real Element of REAL
(l `1) - (|[(l `1),((l `2) + (r / 2))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[(l `1),((l `2) + (r / 2))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[(l `1),((l `2) + (r / 2))]| `1)),((l `1) - (|[(l `1),((l `2) + (r / 2))]| `1))) is V11() real ext-real set
(l `2) - (|[(l `1),((l `2) + (r / 2))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[(l `1),((l `2) + (r / 2))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[(l `1),((l `2) + (r / 2))]| `2)),((l `2) - (|[(l `1),((l `2) + (r / 2))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[(l `1),((l `2) + (r / 2))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) + (r / 2))]| `2)) ^2) is V11() real ext-real Element of REAL
(|[(l `1),((l `2) + (r / 2))]| `2) - (l `2) is V11() real ext-real Element of REAL
((|[(l `1),((l `2) + (r / 2))]| `2) - (l `2)) ^2 is V11() real ext-real Element of REAL
K37(((|[(l `1),((l `2) + (r / 2))]| `2) - (l `2)),((|[(l `1),((l `2) + (r / 2))]| `2) - (l `2))) is V11() real ext-real set
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
sqrt ((((l `1) - (|[(l `1),((l `2) + (r / 2))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) + (r / 2))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[(l `1),((l `2) + (r / 2))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) + (r / 2))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[(l `1),((l `2) + (r / 2))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) + (r / 2))]| `2)) ^2))),(sqrt ((((l `1) - (|[(l `1),((l `2) + (r / 2))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) + (r / 2))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
x1 /\ Q is Element of K6( the carrier of (TOP-REAL 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
(l `2) - (r / 2) is V11() real ext-real Element of REAL
|[(l `1),((l `2) - (r / 2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[(l `1),((l `2) - (r / 2))]| `1 is V11() real ext-real Element of REAL
|[(l `1),((l `2) - (r / 2))]| `2 is V11() real ext-real Element of REAL
(l `1) - (|[(l `1),((l `2) - (r / 2))]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[(l `1),((l `2) - (r / 2))]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[(l `1),((l `2) - (r / 2))]| `1)),((l `1) - (|[(l `1),((l `2) - (r / 2))]| `1))) is V11() real ext-real set
(l `2) - (|[(l `1),((l `2) - (r / 2))]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[(l `1),((l `2) - (r / 2))]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[(l `1),((l `2) - (r / 2))]| `2)),((l `2) - (|[(l `1),((l `2) - (r / 2))]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[(l `1),((l `2) - (r / 2))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) - (r / 2))]| `2)) ^2) is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
sqrt ((((l `1) - (|[(l `1),((l `2) - (r / 2))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) - (r / 2))]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[(l `1),((l `2) - (r / 2))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) - (r / 2))]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[(l `1),((l `2) - (r / 2))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) - (r / 2))]| `2)) ^2))),(sqrt ((((l `1) - (|[(l `1),((l `2) - (r / 2))]| `1)) ^2) + (((l `2) - (|[(l `1),((l `2) - (r / 2))]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
Q is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
QQ is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
q is Element of the carrier of (Euclid 2)
r is V11() real ext-real set
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
(l `1) + (r / 2) is V11() real ext-real Element of REAL
|[((l `1) + (r / 2)),(l `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((l `1) + (r / 2)),(l `2)]| `1 is V11() real ext-real Element of REAL
|[((l `1) + (r / 2)),(l `2)]| `2 is V11() real ext-real Element of REAL
(l `1) - (|[((l `1) + (r / 2)),(l `2)]| `1) is V11() real ext-real Element of REAL
((l `1) - (|[((l `1) + (r / 2)),(l `2)]| `1)) ^2 is V11() real ext-real Element of REAL
K37(((l `1) - (|[((l `1) + (r / 2)),(l `2)]| `1)),((l `1) - (|[((l `1) + (r / 2)),(l `2)]| `1))) is V11() real ext-real set
(l `2) - (|[((l `1) + (r / 2)),(l `2)]| `2) is V11() real ext-real Element of REAL
((l `2) - (|[((l `1) + (r / 2)),(l `2)]| `2)) ^2 is V11() real ext-real Element of REAL
K37(((l `2) - (|[((l `1) + (r / 2)),(l `2)]| `2)),((l `2) - (|[((l `1) + (r / 2)),(l `2)]| `2))) is V11() real ext-real set
0 + 0 is V11() real ext-real Element of REAL
(((l `1) - (|[((l `1) + (r / 2)),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) + (r / 2)),(l `2)]| `2)) ^2) is V11() real ext-real Element of REAL
(|[((l `1) + (r / 2)),(l `2)]| `1) - (l `1) is V11() real ext-real Element of REAL
((|[((l `1) + (r / 2)),(l `2)]| `1) - (l `1)) ^2 is V11() real ext-real Element of REAL
K37(((|[((l `1) + (r / 2)),(l `2)]| `1) - (l `1)),((|[((l `1) + (r / 2)),(l `2)]| `1) - (l `1))) is V11() real ext-real set
r ^2 is V11() real ext-real Element of REAL
K37(r,r) is V11() real ext-real set
sqrt ((((l `1) - (|[((l `1) + (r / 2)),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) + (r / 2)),(l `2)]| `2)) ^2)) is V11() real ext-real Element of REAL
(sqrt ((((l `1) - (|[((l `1) + (r / 2)),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) + (r / 2)),(l `2)]| `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt ((((l `1) - (|[((l `1) + (r / 2)),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) + (r / 2)),(l `2)]| `2)) ^2))),(sqrt ((((l `1) - (|[((l `1) + (r / 2)),(l `2)]| `1)) ^2) + (((l `2) - (|[((l `1) + (r / 2)),(l `2)]| `2)) ^2)))) is V11() real ext-real set
qa is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,qa) is set
dist (q,qa) is V11() real ext-real Element of REAL
Ball (q,r) is Element of K6( the carrier of (Euclid 2))
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & y0 <= b1 `2 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = y0 ) or ( b1 `1 = P & b1 `2 <= w1 & y0 <= b1 `2 ) ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not P <= b1 `1 & not b1 `2 <= y0 & not w1 <= b1 `2 ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= P or not y0 <= b1 `2 or not b1 `2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
x1 is Element of K6( the carrier of (TOP-REAL 2))
x2 is Element of K6( the carrier of (TOP-REAL 2))
Cl x1 is Element of K6( the carrier of (TOP-REAL 2))
(Cl x1) \ x1 is Element of K6( the carrier of (TOP-REAL 2))
Cl x2 is Element of K6( the carrier of (TOP-REAL 2))
(Cl x2) \ x2 is Element of K6( the carrier of (TOP-REAL 2))
w2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ w2 is set
v is Element of K6( the carrier of (TOP-REAL 2))
x1 \/ x2 is Element of K6( the carrier of (TOP-REAL 2))
(x1 \/ x2) ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (x1 \/ x2) is set
[#] (TOP-REAL 2) is non empty non proper closed Element of K6( the carrier of (TOP-REAL 2))
([#] (TOP-REAL 2)) \ x1 is Element of K6( the carrier of (TOP-REAL 2))
([#] (TOP-REAL 2)) \ x2 is Element of K6( the carrier of (TOP-REAL 2))
(([#] (TOP-REAL 2)) \ x1) /\ (([#] (TOP-REAL 2)) \ x2) is Element of K6( the carrier of (TOP-REAL 2))
w2 \/ x2 is Element of K6( the carrier of (TOP-REAL 2))
(w2 \/ x2) \ x2 is Element of K6( the carrier of (TOP-REAL 2))
v1 is set
x2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ x2 is set
(Cl x2) /\ (x2 `) is Element of K6( the carrier of (TOP-REAL 2))
w2 \/ x1 is Element of K6( the carrier of (TOP-REAL 2))
(w2 \/ x1) \ x1 is Element of K6( the carrier of (TOP-REAL 2))
v1 is set
x1 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ x1 is set
(Cl x1) /\ (x1 `) is Element of K6( the carrier of (TOP-REAL 2))
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & P <= b1 `2 ) or ( b1 `1 <= y0 & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= y0 & p <= b1 `1 & b1 `2 = P ) or ( b1 `1 = y0 & b1 `2 <= w1 & P <= b1 `2 ) ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not y0 <= b1 `1 & not b1 `2 <= P & not w1 <= b1 `2 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
w2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ w2 is set
(TOP-REAL 2) | (w2 `) is strict TopSpace-like SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | (w2 `)) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
the carrier of ((TOP-REAL 2) | (w2 `)) is set
K6( the carrier of ((TOP-REAL 2) | (w2 `))) is non empty set
x1 is Element of K6( the carrier of (TOP-REAL 2))
x2 is set
v is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v `1 is V11() real ext-real Element of REAL
v `2 is V11() real ext-real Element of REAL
v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v1 `1 is V11() real ext-real Element of REAL
v1 `2 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & P <= b1 `2 ) or ( b1 `1 <= y0 & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= y0 & p <= b1 `1 & b1 `2 = P ) or ( b1 `1 = y0 & b1 `2 <= w1 & P <= b1 `2 ) ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not y0 <= b1 `1 & not b1 `2 <= P & not w1 <= b1 `2 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
w2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ w2 is set
(TOP-REAL 2) | (w2 `) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (w2 `)) is set
K6( the carrier of ((TOP-REAL 2) | (w2 `))) is non empty set
x1 is Element of K6( the carrier of (TOP-REAL 2))
[#] ((TOP-REAL 2) | (w2 `)) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & P <= b1 `2 ) or ( b1 `1 <= y0 & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= y0 & p <= b1 `1 & b1 `2 = P ) or ( b1 `1 = y0 & b1 `2 <= w1 & P <= b1 `2 ) ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= y0 or not P <= b1 `2 or not b1 `2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
w2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ w2 is set
(TOP-REAL 2) | (w2 `) is strict TopSpace-like SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | (w2 `)) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
the carrier of ((TOP-REAL 2) | (w2 `)) is set
K6( the carrier of ((TOP-REAL 2) | (w2 `))) is non empty set
x1 is Element of K6( the carrier of (TOP-REAL 2))
x2 is set
v is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v `1 is V11() real ext-real Element of REAL
v `2 is V11() real ext-real Element of REAL
v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v1 `1 is V11() real ext-real Element of REAL
v1 `2 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & P <= b1 `2 ) or ( b1 `1 <= y0 & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= y0 & p <= b1 `1 & b1 `2 = P ) or ( b1 `1 = y0 & b1 `2 <= w1 & P <= b1 `2 ) ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= y0 or not P <= b1 `2 or not b1 `2 <= w1 ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
w2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ w2 is set
(TOP-REAL 2) | (w2 `) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (w2 `)) is set
K6( the carrier of ((TOP-REAL 2) | (w2 `))) is non empty set
x1 is Element of K6( the carrier of (TOP-REAL 2))
[#] ((TOP-REAL 2) | (w2 `)) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
p is Element of K6( the carrier of (TOP-REAL 2))
p ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ p is set
(TOP-REAL 2) | (p `) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (p `)) is set
K6( the carrier of ((TOP-REAL 2) | (p `))) is non empty set
P is Element of K6( the carrier of (TOP-REAL 2))
w1 is Element of K6( the carrier of (TOP-REAL 2))
P \/ w1 is Element of K6( the carrier of (TOP-REAL 2))
Cl P is Element of K6( the carrier of (TOP-REAL 2))
(Cl P) \ P is Element of K6( the carrier of (TOP-REAL 2))
Cl w1 is Element of K6( the carrier of (TOP-REAL 2))
(Cl w1) \ w1 is Element of K6( the carrier of (TOP-REAL 2))
[#] ((TOP-REAL 2) | (p `)) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (p `)))
y0 is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | y0 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | y0) is non empty set
K6( the carrier of ((TOP-REAL 2) | y0)) is non empty set
w2 is Element of K6( the carrier of ((TOP-REAL 2) | y0))
x1 is Element of K6( the carrier of ((TOP-REAL 2) | y0))
x2 is Element of K6( the carrier of ((TOP-REAL 2) | y0))
{} ((TOP-REAL 2) | y0) is empty proper closed V163() V164() V165() V166() V167() V168() V169() Element of K6( the carrier of ((TOP-REAL 2) | y0))
w2 \/ x1 is Element of K6( the carrier of ((TOP-REAL 2) | y0))
x2 /\ (w2 \/ x1) is Element of K6( the carrier of ((TOP-REAL 2) | y0))
x2 /\ w2 is Element of K6( the carrier of ((TOP-REAL 2) | y0))
x2 /\ x1 is Element of K6( the carrier of ((TOP-REAL 2) | y0))
(x2 /\ w2) \/ (x2 /\ x1) is Element of K6( the carrier of ((TOP-REAL 2) | y0))
x2 \/ w2 is Element of K6( the carrier of ((TOP-REAL 2) | y0))
x2 /\ w1 is Element of K6( the carrier of (TOP-REAL 2))
x2 \/ x1 is Element of K6( the carrier of ((TOP-REAL 2) | y0))
x2 /\ w1 is Element of K6( the carrier of (TOP-REAL 2))
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & P <= b1 `2 ) or ( b1 `1 <= y0 & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= y0 & p <= b1 `1 & b1 `2 = P ) or ( b1 `1 = y0 & b1 `2 <= w1 & P <= b1 `2 ) ) } is set
w2 is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not y0 <= b1 `1 & not b1 `2 <= P & not w1 <= b1 `2 ) } is set
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= y0 or not P <= b1 `2 or not b1 `2 <= w1 ) } is set
w2 ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ w2 is set
x1 is Element of K6( the carrier of (TOP-REAL 2))
x2 is Element of K6( the carrier of (TOP-REAL 2))
v is Element of K6( the carrier of (TOP-REAL 2))
x1 \/ x2 is Element of K6( the carrier of (TOP-REAL 2))
Cl x1 is Element of K6( the carrier of (TOP-REAL 2))
(Cl x1) \ x1 is Element of K6( the carrier of (TOP-REAL 2))
Cl x2 is Element of K6( the carrier of (TOP-REAL 2))
(Cl x2) \ x2 is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (w2 `) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (w2 `)) is set
K6( the carrier of ((TOP-REAL 2) | (w2 `))) is non empty set
v1 is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
l is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))
P is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
w2 is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & y0 <= b1 `2 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = y0 ) or ( b1 `1 = P & b1 `2 <= w1 & y0 <= b1 `2 ) ) } is set
x1 is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not p <= b1 `1 or not b1 `1 <= P or not y0 <= b1 `2 or not b1 `2 <= w1 ) } is set
Cl x1 is Element of K6( the carrier of (TOP-REAL 2))
w2 \/ x1 is Element of K6( the carrier of (TOP-REAL 2))
P is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
w1 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
w2 is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = p & b1 `2 <= w1 & y0 <= b1 `2 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = w1 ) or ( b1 `1 <= P & p <= b1 `1 & b1 `2 = y0 ) or ( b1 `1 = P & b1 `2 <= w1 & y0 <= b1 `2 ) ) } is set
x1 is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2) : ( not b1 `1 <= p & not P <= b1 `1 & not b1 `2 <= y0 & not w1 <= b1 `2 ) } is set
Cl x1 is Element of K6( the carrier of (TOP-REAL 2))
w2 \/ x1 is Element of K6( the carrier of (TOP-REAL 2))
P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
y0 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (p,y0) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * p) + (b1 * y0)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{p,y0} is non empty set
(LSeg (p,y0)) \ {p,y0} is Element of K6( the carrier of (TOP-REAL 2))
w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (P,w1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * P) + (b1 * w1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
y0 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
{ |[b1,y0]| where b1 is V11() real ext-real Element of REAL : b1 <= p } is set
P is Element of K6( the carrier of (TOP-REAL 2))
w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (w1,w2) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * w1) + (b1 * w2)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
x1 is V11() real ext-real Element of REAL
|[x1,y0]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x2 is V11() real ext-real Element of REAL
|[x2,y0]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v is set
v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l is V11() real ext-real Element of REAL
1 - l is V11() real ext-real Element of REAL
(1 - l) * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * w2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * w1) + (l * w2) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(1 - l) * x1 is V11() real ext-real Element of REAL
(1 - l) * y0 is V11() real ext-real Element of REAL
|[((1 - l) * x1),((1 - l) * y0)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * |[x2,y0]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((1 - l) * x1),((1 - l) * y0)]| + (l * |[x2,y0]|) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * x2 is V11() real ext-real Element of REAL
l * y0 is V11() real ext-real Element of REAL
|[(l * x2),(l * y0)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((1 - l) * x1),((1 - l) * y0)]| + |[(l * x2),(l * y0)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * x1) + (l * x2) is V11() real ext-real Element of REAL
((1 - l) * y0) + (l * y0) is V11() real ext-real Element of REAL
|[(((1 - l) * x1) + (l * x2)),(((1 - l) * y0) + (l * y0))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
1 * y0 is V11() real ext-real Element of REAL
|[(((1 - l) * x1) + (l * x2)),(1 * y0)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
{ |[p,b1]| where b1 is V11() real ext-real Element of REAL : b1 <= y0 } is set
P is Element of K6( the carrier of (TOP-REAL 2))
w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (w1,w2) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * w1) + (b1 * w2)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
x1 is V11() real ext-real Element of REAL
|[p,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x2 is V11() real ext-real Element of REAL
|[p,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v is set
v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l is V11() real ext-real Element of REAL
1 - l is V11() real ext-real Element of REAL
(1 - l) * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * w2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * w1) + (l * w2) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(1 - l) * p is V11() real ext-real Element of REAL
(1 - l) * x1 is V11() real ext-real Element of REAL
|[((1 - l) * p),((1 - l) * x1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * |[p,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((1 - l) * p),((1 - l) * x1)]| + (l * |[p,x2]|) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * p is V11() real ext-real Element of REAL
l * x2 is V11() real ext-real Element of REAL
|[(l * p),(l * x2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((1 - l) * p),((1 - l) * x1)]| + |[(l * p),(l * x2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * p) + (l * p) is V11() real ext-real Element of REAL
((1 - l) * x1) + (l * x2) is V11() real ext-real Element of REAL
|[(((1 - l) * p) + (l * p)),(((1 - l) * x1) + (l * x2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
1 * p is V11() real ext-real Element of REAL
|[(1 * p),(((1 - l) * x1) + (l * x2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
y0 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
{ |[b1,y0]| where b1 is V11() real ext-real Element of REAL : p <= b1 } is set
P is Element of K6( the carrier of (TOP-REAL 2))
w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (w1,w2) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * w1) + (b1 * w2)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
x1 is V11() real ext-real Element of REAL
|[x1,y0]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x2 is V11() real ext-real Element of REAL
|[x2,y0]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v is set
v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
{ (((1 - b1) * w2) + (b1 * w1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
l is V11() real ext-real Element of REAL
1 - l is V11() real ext-real Element of REAL
(1 - l) * w2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * w2) + (l * w1) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(1 - l) * x2 is V11() real ext-real Element of REAL
(1 - l) * y0 is V11() real ext-real Element of REAL
|[((1 - l) * x2),((1 - l) * y0)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * |[x1,y0]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((1 - l) * x2),((1 - l) * y0)]| + (l * |[x1,y0]|) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * x1 is V11() real ext-real Element of REAL
l * y0 is V11() real ext-real Element of REAL
|[(l * x1),(l * y0)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((1 - l) * x2),((1 - l) * y0)]| + |[(l * x1),(l * y0)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * x2) + (l * x1) is V11() real ext-real Element of REAL
((1 - l) * y0) + (l * y0) is V11() real ext-real Element of REAL
|[(((1 - l) * x2) + (l * x1)),(((1 - l) * y0) + (l * y0))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
1 * y0 is V11() real ext-real Element of REAL
|[(((1 - l) * x2) + (l * x1)),(1 * y0)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
{ |[p,b1]| where b1 is V11() real ext-real Element of REAL : y0 <= b1 } is set
P is Element of K6( the carrier of (TOP-REAL 2))
w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
w2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
LSeg (w1,w2) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * w1) + (b1 * w2)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
x1 is V11() real ext-real Element of REAL
|[p,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
x2 is V11() real ext-real Element of REAL
|[p,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
v is set
v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
{ (((1 - b1) * w2) + (b1 * w1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
l is V11() real ext-real Element of REAL
1 - l is V11() real ext-real Element of REAL
(1 - l) * w2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * w2) + (l * w1) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
(1 - l) * p is V11() real ext-real Element of REAL
(1 - l) * x2 is V11() real ext-real Element of REAL
|[((1 - l) * p),((1 - l) * x2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * |[p,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((1 - l) * p),((1 - l) * x2)]| + (l * |[p,x1]|) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
l * p is V11() real ext-real Element of REAL
l * x1 is V11() real ext-real Element of REAL
|[(l * p),(l * x1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
|[((1 - l) * p),((1 - l) * x2)]| + |[(l * p),(l * x1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
((1 - l) * p) + (l * p) is V11() real ext-real Element of REAL
((1 - l) * x2) + (l * x1) is V11() real ext-real Element of REAL
|[(((1 - l) * p) + (l * p)),(((1 - l) * x2) + (l * x1))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
1 * p is V11() real ext-real Element of REAL
|[(1 * p),(((1 - l) * x2) + (l * x1))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
p is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)
north_halfline p is Element of K6( the carrier of (TOP-REAL 2))
p `1 is V11() real ext-real Element of REAL
p `2 is V11() real ext-real Element of REAL
{ |[(p `1),b1]| where b1 is V11() real ext-real Element of REAL : p `2 <= b1 } is set
east_halfline p is Element of K6( the carrier of (TOP-REAL 2))
p `2 is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
{ |[b1,(p `2)]| where b1 is V11() real ext-real Element of REAL : p `1 <= b1 } is set
south_halfline p is Element of K6( the carrier of (TOP-REAL 2))
p `1 is V11() real ext-real Element of REAL
p `2 is V11() real ext-real Element of REAL
{ |[(p `1),b1]| where b1 is V11() real ext-real Element of REAL : b1 <= p `2 } is set
west_halfline p is Element of K6( the carrier of (TOP-REAL 2))
p `2 is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
{ |[b1,(p `2)]| where b1 is V11() real ext-real Element of REAL : b1 <= p `1 } is set