REAL is V140() V141() V142() V146() set
NAT is V140() V141() V142() V143() V144() V145() V146() Element of K19(REAL)
K19(REAL) is set
omega is V140() V141() V142() V143() V144() V145() V146() set
K19(omega) is set
K19(NAT) is set
1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
K20(1,1) is set
K19(K20(1,1)) is set
K20(K20(1,1),1) is set
K19(K20(K20(1,1),1)) is set
K20(K20(1,1),REAL) is set
K19(K20(K20(1,1),REAL)) is set
K20(REAL,REAL) is set
K20(K20(REAL,REAL),REAL) is set
K19(K20(K20(REAL,REAL),REAL)) is set
2 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
K20(2,2) is set
K20(K20(2,2),REAL) is set
K19(K20(K20(2,2),REAL)) is set
COMPLEX is V140() V146() set
RAT is V140() V141() V142() V143() V146() set
INT is V140() V141() V142() V143() V144() V146() set
K19(K20(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V106() V152() V153() V154() V155() V156() V157() V158() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K19( the carrier of (TOP-REAL 2)) is set
{} is functional empty FinSequence-membered V140() V141() V142() V143() V144() V145() V146() set
the functional empty FinSequence-membered V140() V141() V142() V143() V144() V145() V146() set is functional empty FinSequence-membered V140() V141() V142() V143() V144() V145() V146() set
3 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
0 is functional empty ext-real non positive non negative ordinal natural V25() real FinSequence-membered V92() V93() V140() V141() V142() V143() V144() V145() V146() Element of NAT
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid 2) is non empty set
p is TopStruct
the carrier of p is set
K19( the carrier of p) is set
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ RR is Element of K19( the carrier of (TOP-REAL 2))
len RR is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (RR,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len RR ) } is set
union { (LSeg (RR,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len RR ) } is set
RR /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR /. (len RR) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ RR is Element of K19( the carrier of (TOP-REAL 2))
len RR is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (RR,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len RR ) } is set
union { (LSeg (RR,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len RR ) } is set
RR /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR /. (len RR) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ RR is Element of K19( the carrier of (TOP-REAL 2))
len RR is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (RR,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len RR ) } is set
union { (LSeg (RR,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len RR ) } is set
RR /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR /. (len RR) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
Seg (len RR) is V33() V40( len RR) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom RR is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Element of K19( the carrier of (TOP-REAL 2))
RR is Element of K19( the carrier of (TOP-REAL 2))
RR /\ RR is Element of K19( the carrier of (TOP-REAL 2))
{q,R} is non empty set
RR \/ RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is non empty Element of K19( the carrier of (TOP-REAL 2))
P12 is non empty Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
(p `2) + (q `2) is ext-real V25() real Element of REAL
((p `2) + (q `2)) / 2 is ext-real V25() real Element of REAL
|[(p `1),(((p `2) + (q `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
union { (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) \/ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
(p `1) + (q `1) is ext-real V25() real Element of REAL
((p `1) + (q `1)) / 2 is ext-real V25() real Element of REAL
|[(((p `1) + (q `1)) / 2),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
union { (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) \/ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
|[(p `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(p `1),(q `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
union { (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
LSeg (|[(p `1),(q `2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (p,|[(p `1),(q `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
|[(q `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(q `1),(p `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
union { (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
LSeg (|[(q `1),(p `2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (p,|[(q `1),(p `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,R) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
p `1 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
(p `1) + (q `1) is ext-real V25() real Element of REAL
((p `1) + (q `1)) / 2 is ext-real V25() real Element of REAL
|[(((p `1) + (q `1)) / 2),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> ) } is set
union { (LSeg (<*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
p `2 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(p `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(p `1),(q `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(p `1),(q `2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(p `1),(q `2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(p `1),(q `2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(p `1),(q `2)]|,q*> ) } is set
union { (LSeg (<*p,|[(p `1),(q `2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(p `1),(q `2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
|[(q `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(q `1),(p `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(q `1),(p `2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(q `1),(p `2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(q `1),(p `2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(q `1),(p `2)]|,q*> ) } is set
union { (LSeg (<*p,|[(q `1),(p `2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(q `1),(p `2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
|[(p `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Element of K19( the carrier of (TOP-REAL 2))
p `2 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
RR is Element of K19( the carrier of (TOP-REAL 2))
p `2 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
(p `2) + (q `2) is ext-real V25() real Element of REAL
((p `2) + (q `2)) / 2 is ext-real V25() real Element of REAL
|[(p `1),(((p `2) + (q `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> ) } is set
union { (LSeg (<*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
p `1 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(p `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(p `1),(q `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(p `1),(q `2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(p `1),(q `2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(p `1),(q `2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(p `1),(q `2)]|,q*> ) } is set
union { (LSeg (<*p,|[(p `1),(q `2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(p `1),(q `2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
|[(q `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(q `1),(p `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(q `1),(p `2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(q `1),(p `2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(q `1),(p `2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(q `1),(p `2)]|,q*> ) } is set
union { (LSeg (<*p,|[(q `1),(p `2)]|,q*>,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p,|[(q `1),(p `2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
|[(p `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Element of K19( the carrier of (TOP-REAL 2))
p `1 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
RR is Element of K19( the carrier of (TOP-REAL 2))
p `1 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
RR is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `2 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. 1) `2 is ext-real V25() real Element of REAL
LSeg (q,1) is Element of K19( the carrier of (TOP-REAL 2))
(q /. 1) `1 is ext-real V25() real Element of REAL
((q /. 1) `1) + (p `1) is ext-real V25() real Element of REAL
(((q /. 1) `1) + (p `1)) / 2 is ext-real V25() real Element of REAL
|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(q /. 1),|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
q | 1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (q | 1) is Element of K19( the carrier of (TOP-REAL 2))
len (q | 1) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((q | 1),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | 1) ) } is set
union { (LSeg ((q | 1),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | 1) ) } is set
LSeg ((q /. 1),p) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (q | 1)) \/ (LSeg ((q /. 1),p)) is Element of K19( the carrier of (TOP-REAL 2))
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
union { (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (1 + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg ((q /. 1),|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|,p) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((q /. 1),|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|)) \/ (LSeg (|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|,p)) is Element of K19( the carrier of (TOP-REAL 2))
LSeg ((q /. 1),(q /. (1 + 1))) is Element of K19( the carrier of (TOP-REAL 2))
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
Seg 1 is non empty V33() V40(1) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q | (Seg 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
(dom q) /\ (Seg 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (q | 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. 1) `1 is ext-real V25() real Element of REAL
LSeg (q,1) is Element of K19( the carrier of (TOP-REAL 2))
(q /. 1) `2 is ext-real V25() real Element of REAL
((q /. 1) `2) + (p `2) is ext-real V25() real Element of REAL
(((q /. 1) `2) + (p `2)) / 2 is ext-real V25() real Element of REAL
|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(q /. 1),|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
q | 1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (q | 1) is Element of K19( the carrier of (TOP-REAL 2))
len (q | 1) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((q | 1),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | 1) ) } is set
union { (LSeg ((q | 1),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | 1) ) } is set
LSeg ((q /. 1),p) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (q | 1)) \/ (LSeg ((q /. 1),p)) is Element of K19( the carrier of (TOP-REAL 2))
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
union { (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
LSeg ((q /. 1),|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|,p) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((q /. 1),|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|)) \/ (LSeg (|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|,p)) is Element of K19( the carrier of (TOP-REAL 2))
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (1 + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg ((q /. 1),(q /. (1 + 1))) is Element of K19( the carrier of (TOP-REAL 2))
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
Seg 1 is non empty V33() V40(1) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q | (Seg 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
(dom q) /\ (Seg 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (q | 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
union { (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
RR is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
RR + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,RR) is Element of K19( the carrier of (TOP-REAL 2))
q /. RR is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q | RR is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(q | RR) ^ <*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (q | RR) is Element of K19( the carrier of (TOP-REAL 2))
len (q | RR) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((q | RR),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | RR) ) } is set
union { (LSeg ((q | RR),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | RR) ) } is set
LSeg ((q /. RR),p) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (q | RR)) \/ (LSeg ((q /. RR),p)) is Element of K19( the carrier of (TOP-REAL 2))
Seg RR is V33() V40(RR) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q | (Seg RR) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
dom (q | RR) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
(dom q) /\ (Seg RR) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
Seg (len R) is V33() V40( len R) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom R is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q /. (RR + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
LSeg ((q /. RR),(q /. (RR + 1))) is Element of K19( the carrier of (TOP-REAL 2))
LSeg ((q /. (RR + 1)),(q /. RR)) is Element of K19( the carrier of (TOP-REAL 2))
(q /. RR) `1 is ext-real V25() real Element of REAL
(q /. RR) `2 is ext-real V25() real Element of REAL
|[((q /. RR) `1),((q /. RR) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. (RR + 1)) `1 is ext-real V25() real Element of REAL
(q /. (RR + 1)) `2 is ext-real V25() real Element of REAL
|[((q /. (RR + 1)) `1),((q /. (RR + 1)) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
len <*p*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
RR + (len <*p*>) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. RR is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q | RR) /. RR is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (R,RR) is Element of K19( the carrier of (TOP-REAL 2))
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ b1 where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 <= len R ) } is set
r9 is set
x is set
R . r9 is set
R . x is set
q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q + (1 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(q + 1) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P2 + (1 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(P2 + 1) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(q | RR) /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (q,P2) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,P2)) /\ (LSeg (q,RR)) is Element of K19( the carrier of (TOP-REAL 2))
{(q /. RR)} is non empty set
LSeg (q,P2) is Element of K19( the carrier of (TOP-REAL 2))
(q | RR) /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q | RR) /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (q,q) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,q)) /\ (LSeg (q,RR)) is Element of K19( the carrier of (TOP-REAL 2))
{(q /. RR)} is non empty set
LSeg (q,q) is Element of K19( the carrier of (TOP-REAL 2))
(q | RR) /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q . q is set
(q | RR) . q is set
R . q is set
(q | RR) . P2 is set
q . P2 is set
r is ext-real non negative ordinal natural V25() real set
r + 2 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,r) is Element of K19( the carrier of (TOP-REAL 2))
r + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,(r + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,(r + 1))) is Element of K19( the carrier of (TOP-REAL 2))
R /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
{(R /. (r + 1))} is non empty set
(r + 1) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
r + (1 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(q | RR) /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(RR + 1) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
RR + (1 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
RR + 2 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | RR),r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,(r + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,r)) /\ (LSeg (q,(r + 1))) is Element of K19( the carrier of (TOP-REAL 2))
{(q /. (r + 1))} is non empty set
LSeg ((q | RR),(r + 1)) is Element of K19( the carrier of (TOP-REAL 2))
r9 is ext-real non negative ordinal natural V25() real set
r is ext-real non negative ordinal natural V25() real set
r + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (R,r9) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,r9) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | RR),r9) is Element of K19( the carrier of (TOP-REAL 2))
0 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | RR),r) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (q,r)) /\ (LSeg (q,r9)) is Element of K19( the carrier of (TOP-REAL 2))
0 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | RR),r) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,r9)) /\ (LSeg (R,r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r9)) /\ ((LSeg (q,r9)) /\ (LSeg (R,r))) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r9)) /\ (LSeg (q,r9)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (R,r9)) /\ (LSeg (q,r9))) /\ (LSeg (R,r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r is ext-real non negative ordinal natural V25() real set
r + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. r is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(R /. r) `1 is ext-real V25() real Element of REAL
R /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(R /. (r + 1)) `1 is ext-real V25() real Element of REAL
(R /. r) `2 is ext-real V25() real Element of REAL
(R /. (r + 1)) `2 is ext-real V25() real Element of REAL
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b1 `1 = (q /. RR) `1 & (q /. RR) `2 <= b1 `2 & b1 `2 <= (q /. (RR + 1)) `2 ) } is set
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b1 `1 = (q /. RR) `1 & (q /. (RR + 1)) `2 <= b1 `2 & b1 `2 <= (q /. RR) `2 ) } is set
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b1 `2 = (q /. RR) `2 & (q /. RR) `1 <= b1 `1 & b1 `1 <= (q /. (RR + 1)) `1 ) } is set
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `2 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b1 `2 = (q /. RR) `2 & (q /. (RR + 1)) `1 <= b1 `1 & b1 `1 <= (q /. RR) `1 ) } is set
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `2 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
(q | RR) /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q | RR) /. r is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. r is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q | RR) /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
Seg (len (q | RR)) is V33() V40( len (q | RR)) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q is set
P2 is set
P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,P2) is Element of K19( the carrier of (TOP-REAL 2))
P2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,P2) is Element of K19( the carrier of (TOP-REAL 2))
LSeg ((q | RR),P2) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,P2) is Element of K19( the carrier of (TOP-REAL 2))
q is set
q is set
q is set
P2 is set
P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | RR),P2) is Element of K19( the carrier of (TOP-REAL 2))
P2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,P2) is Element of K19( the carrier of (TOP-REAL 2))
p is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p /. 2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(p /. 2) `2 is ext-real V25() real Element of REAL
(p /. 1) `2 is ext-real V25() real Element of REAL
(p /. 1) `1 is ext-real V25() real Element of REAL
(p /. 2) `1 is ext-real V25() real Element of REAL
((p /. 1) `1) + ((p /. 2) `1) is ext-real V25() real Element of REAL
(((p /. 1) `1) + ((p /. 2) `1)) / 2 is ext-real V25() real Element of REAL
|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(p /. 1),|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]|,(p /. 2)*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ p is Element of K19( the carrier of (TOP-REAL 2))
len p is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (p,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len p ) } is set
union { (LSeg (p,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len p ) } is set
p | 1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (p | 1) is Element of K19( the carrier of (TOP-REAL 2))
len (p | 1) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((p | 1),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p | 1) ) } is set
union { (LSeg ((p | 1),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p | 1) ) } is set
LSeg ((p /. 1),(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (p | 1)) \/ (LSeg ((p /. 1),(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
p | 2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (p | 2) is Element of K19( the carrier of (TOP-REAL 2))
len (p | 2) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((p | 2),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p | 2) ) } is set
union { (LSeg ((p | 2),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p | 2) ) } is set
LSeg ((p /. 2),(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (p | 2)) \/ (LSeg ((p /. 2),(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
LSeg ((p /. 1),|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]|,(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((p /. 1),|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]|)) \/ (LSeg (|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]|,(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
Seg (len p) is V33() V40( len p) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom p is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (p,1) is Element of K19( the carrier of (TOP-REAL 2))
Seg 2 is non empty V33() V40(2) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p | (Seg 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
(dom p) /\ (Seg 2) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (p | 2) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
P11 is set
P12 is set
R9 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((p | 2),R9) is Element of K19( the carrier of (TOP-REAL 2))
R9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(len (p | 2)) - 1 is ext-real V25() real Element of REAL
(1 + 1) - 1 is ext-real V25() real Element of REAL
(R9 + 1) - 1 is ext-real V25() real Element of REAL
{(p /. 2)} is non empty set
Seg 1 is non empty V33() V40(1) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p | (Seg 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
(dom p) /\ (Seg 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (p | 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
LSeg ((p | 2),1) is Element of K19( the carrier of (TOP-REAL 2))
p is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p /. 2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(p /. 2) `1 is ext-real V25() real Element of REAL
(p /. 1) `1 is ext-real V25() real Element of REAL
(p /. 1) `2 is ext-real V25() real Element of REAL
(p /. 2) `2 is ext-real V25() real Element of REAL
((p /. 1) `2) + ((p /. 2) `2) is ext-real V25() real Element of REAL
(((p /. 1) `2) + ((p /. 2) `2)) / 2 is ext-real V25() real Element of REAL
|[((p /. 1) `1),((((p /. 1) `2) + ((p /. 2) `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(p /. 1),|[((p /. 1) `1),((((p /. 1) `2) + ((p /. 2) `2)) / 2)]|,(p /. 2)*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ p is Element of K19( the carrier of (TOP-REAL 2))
len p is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (p,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len p ) } is set
union { (LSeg (p,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len p ) } is set
p | 1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (p | 1) is Element of K19( the carrier of (TOP-REAL 2))
len (p | 1) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((p | 1),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p | 1) ) } is set
union { (LSeg ((p | 1),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p | 1) ) } is set
LSeg ((p /. 1),(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (p | 1)) \/ (LSeg ((p /. 1),(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
p | 2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (p | 2) is Element of K19( the carrier of (TOP-REAL 2))
len (p | 2) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((p | 2),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p | 2) ) } is set
union { (LSeg ((p | 2),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p | 2) ) } is set
LSeg ((p /. 2),(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (p | 2)) \/ (LSeg ((p /. 2),(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
LSeg ((p /. 1),|[((p /. 1) `1),((((p /. 1) `2) + ((p /. 2) `2)) / 2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[((p /. 1) `1),((((p /. 1) `2) + ((p /. 2) `2)) / 2)]|,(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((p /. 1),|[((p /. 1) `1),((((p /. 1) `2) + ((p /. 2) `2)) / 2)]|)) \/ (LSeg (|[((p /. 1) `1),((((p /. 1) `2) + ((p /. 2) `2)) / 2)]|,(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
Seg (len p) is V33() V40( len p) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom p is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (p,1) is Element of K19( the carrier of (TOP-REAL 2))
Seg 2 is non empty V33() V40(2) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p | (Seg 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
(dom p) /\ (Seg 2) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (p | 2) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
P11 is set
P12 is set
R9 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((p | 2),R9) is Element of K19( the carrier of (TOP-REAL 2))
R9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(len (p | 2)) - 1 is ext-real V25() real Element of REAL
(1 + 1) - 1 is ext-real V25() real Element of REAL
(R9 + 1) - 1 is ext-real V25() real Element of REAL
{(p /. 2)} is non empty set
Seg 1 is non empty V33() V40(1) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p | (Seg 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
(dom p) /\ (Seg 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (p | 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
LSeg ((p | 2),1) is Element of K19( the carrier of (TOP-REAL 2))
p is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom p is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ p is Element of K19( the carrier of (TOP-REAL 2))
len p is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (p,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len p ) } is set
union { (LSeg (p,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len p ) } is set
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
p | R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p /. R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ (p | R) is Element of K19( the carrier of (TOP-REAL 2))
len (p | R) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((p | R),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p | R) ) } is set
union { (LSeg ((p | R),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p | R) ) } is set
LSeg ((p /. R),(p /. R)) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (p | R)) \/ (LSeg ((p /. R),(p /. R))) is Element of K19( the carrier of (TOP-REAL 2))
Seg (len p) is V33() V40( len p) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
Seg R is V33() V40(R) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p | (Seg R) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
(Seg (len p)) /\ (Seg R) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
{(p /. R)} is non empty set
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,R) is Element of K19( the carrier of (TOP-REAL 2))
q | R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (q | R) is Element of K19( the carrier of (TOP-REAL 2))
len (q | R) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((q | R),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | R) ) } is set
union { (LSeg ((q | R),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | R) ) } is set
q /. R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg ((q /. R),p) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (q | R)) \/ (LSeg ((q /. R),p)) is Element of K19( the carrier of (TOP-REAL 2))
R + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q /. (R + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. (R + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(q /. 1) `1 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
(q /. 1) `2 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
((q /. 1) `2) + (p `2) is ext-real V25() real Element of REAL
(((q /. 1) `2) + (p `2)) / 2 is ext-real V25() real Element of REAL
|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(q /. 1),|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
(q /. 1) `2 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
(q /. 1) `1 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
((q /. 1) `1) + (p `1) is ext-real V25() real Element of REAL
(((q /. 1) `1) + (p `1)) / 2 is ext-real V25() real Element of REAL
|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(q /. 1),|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
(q /. 1) `1 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
(q /. 1) `2 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
q /. (R + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. 1) `1 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
(q /. 1) `2 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
((q /. 1) `2) + (p `2) is ext-real V25() real Element of REAL
(((q /. 1) `2) + (p `2)) / 2 is ext-real V25() real Element of REAL
|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(q /. 1),|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
(q /. 1) `2 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
(q /. 1) `1 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
((q /. 1) `1) + (p `1) is ext-real V25() real Element of REAL
(((q /. 1) `1) + (p `1)) / 2 is ext-real V25() real Element of REAL
|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(q /. 1),|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
(q /. 1) `1 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
(q /. 1) `2 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
q | (R + 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
q /. (R + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (1 + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg ((q /. 1),(q /. (1 + 1))) is Element of K19( the carrier of (TOP-REAL 2))
(q /. 1) `1 is ext-real V25() real Element of REAL
(q /. (1 + 1)) `1 is ext-real V25() real Element of REAL
(q /. 1) `2 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
((q /. 1) `2) + (p `2) is ext-real V25() real Element of REAL
(((q /. 1) `2) + (p `2)) / 2 is ext-real V25() real Element of REAL
|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(q /. 1),|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
P12 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P12 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P12 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P12 /. (len P12) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P12 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P12,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P12 ) } is set
union { (LSeg (P12,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P12 ) } is set
(q /. 1) `2 is ext-real V25() real Element of REAL
(q /. (1 + 1)) `2 is ext-real V25() real Element of REAL
(q /. 1) `1 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
((q /. 1) `1) + (p `1) is ext-real V25() real Element of REAL
(((q /. 1) `1) + (p `1)) / 2 is ext-real V25() real Element of REAL
|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(q /. 1),|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p `2 is ext-real V25() real Element of REAL
P12 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P12 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P12 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P12 /. (len P12) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P12 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P12,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P12 ) } is set
union { (LSeg (P12,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P12 ) } is set
(q /. 1) `1 is ext-real V25() real Element of REAL
(q /. (1 + 1)) `1 is ext-real V25() real Element of REAL
(q /. 1) `2 is ext-real V25() real Element of REAL
(q /. (1 + 1)) `2 is ext-real V25() real Element of REAL
P12 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P12 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P12 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P12 /. (len P12) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P12 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P12,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P12 ) } is set
union { (LSeg (P12,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P12 ) } is set
<*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(q | R) ^ <*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
q /. (R + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. (R + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P11 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P11 /. (len P11) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P11 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
union { (LSeg (P11,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P11 ) } is set
P12 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P12 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P12 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P12 /. (len P12) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P12 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P12,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P12 ) } is set
union { (LSeg (P12,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P12 ) } is set
R9 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R9 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R9 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R9 /. (len R9) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R9 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R9,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R9 ) } is set
union { (LSeg (R9,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R9 ) } is set
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
RR is set
P11 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,P11) is Element of K19( the carrier of (TOP-REAL 2))
P11 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q | P11 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (q | P11) is Element of K19( the carrier of (TOP-REAL 2))
len (q | P11) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((q | P11),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | P11) ) } is set
union { (LSeg ((q | P11),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | P11) ) } is set
q /. P11 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg ((q /. P11),p) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (q | P11)) \/ (LSeg ((q /. P11),p)) is Element of K19( the carrier of (TOP-REAL 2))
P12 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P12 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P12 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P12 /. (len P12) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P12 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P12,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P12 ) } is set
union { (LSeg (P12,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P12 ) } is set
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
<*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. (len q)) `1 is ext-real V25() real Element of REAL
(q /. (len q)) `2 is ext-real V25() real Element of REAL
LSeg ((q /. (len q)),p) is Element of K19( the carrier of (TOP-REAL 2))
L~ q is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
(LSeg ((q /. (len q)),p)) /\ (L~ q) is Element of K19( the carrier of (TOP-REAL 2))
{(q /. (len q))} is non empty set
q ^ <*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
union { (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
(L~ q) \/ (Ball (RR,RR)) is set
Seg (len R) is V33() V40( len R) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom R is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
R /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len <*p*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(len q) + (len <*p*>) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(len q) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (R,(len q)) is Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 <= len R ) } is set
r9 is set
x is set
R . r9 is set
R . x is set
q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
((len q) + 1) - 1 is ext-real V25() real Element of REAL
q /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
((len q) + 1) - 1 is ext-real V25() real Element of REAL
q /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q . P2 is set
R . P2 is set
q . q is set
2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
r is ext-real non negative ordinal natural V25() real set
r + 2 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,r) is Element of K19( the carrier of (TOP-REAL 2))
r + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,(r + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,(r + 1))) is Element of K19( the carrier of (TOP-REAL 2))
R /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
{(R /. (r + 1))} is non empty set
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
r + (1 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(r + 1) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(1 + 1) - 1 is ext-real V25() real Element of REAL
r + ((1 + 1) - 1) is ext-real V25() real Element of REAL
LSeg (q,r) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (L~ q) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ {(R /. (r + 1))} is Element of K19( the carrier of (TOP-REAL 2))
r + (2 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(r + (2 + 1)) - 1 is ext-real V25() real Element of REAL
LSeg (q,r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,(r + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,r)) /\ (LSeg (q,(r + 1))) is Element of K19( the carrier of (TOP-REAL 2))
q /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
{(q /. (r + 1))} is non empty set
r9 is ext-real non negative ordinal natural V25() real set
r is ext-real non negative ordinal natural V25() real set
r + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (R,r9) is Element of K19( the carrier of (TOP-REAL 2))
(r + 1) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
r + (1 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,r9) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,r)) /\ (LSeg (q,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
0 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
0 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
the Element of (LSeg (R,r)) /\ (LSeg (R,r9)) is Element of (LSeg (R,r)) /\ (LSeg (R,r9))
LSeg (q,(r + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,r)) /\ (LSeg (q,(r + 1))) is Element of K19( the carrier of (TOP-REAL 2))
q /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
{(q /. (r + 1))} is non empty set
(len q) - 1 is ext-real V25() real Element of REAL
r + 2 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(r + 2) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,P2) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,r)) /\ (LSeg (q,P2)) is Element of K19( the carrier of (TOP-REAL 2))
(1 + 1) - 1 is ext-real V25() real Element of REAL
P2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r is ext-real non negative ordinal natural V25() real set
r + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. r is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(R /. r) `1 is ext-real V25() real Element of REAL
(R /. (r + 1)) `1 is ext-real V25() real Element of REAL
(R /. r) `2 is ext-real V25() real Element of REAL
(R /. (r + 1)) `2 is ext-real V25() real Element of REAL
q /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. r is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(R /. r) `1 is ext-real V25() real Element of REAL
(R /. (r + 1)) `1 is ext-real V25() real Element of REAL
(R /. r) `2 is ext-real V25() real Element of REAL
(R /. (r + 1)) `2 is ext-real V25() real Element of REAL
(R /. r) `1 is ext-real V25() real Element of REAL
(R /. (r + 1)) `1 is ext-real V25() real Element of REAL
(R /. r) `2 is ext-real V25() real Element of REAL
(R /. (r + 1)) `2 is ext-real V25() real Element of REAL
(R /. r) `1 is ext-real V25() real Element of REAL
(R /. (r + 1)) `1 is ext-real V25() real Element of REAL
(R /. r) `2 is ext-real V25() real Element of REAL
(R /. (r + 1)) `2 is ext-real V25() real Element of REAL
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
r is set
r9 is set
x is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,x) is Element of K19( the carrier of (TOP-REAL 2))
x + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,x) is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. (len q)) `2 is ext-real V25() real Element of REAL
|[(p `1),((q /. (len q)) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. (len q)) `1 is ext-real V25() real Element of REAL
<*|[(p `1),((q /. (len q)) `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q ^ <*|[(p `1),((q /. (len q)) `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg ((q /. (len q)),|[(p `1),((q /. (len q)) `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(p `1),((q /. (len q)) `2)]|,p) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((q /. (len q)),|[(p `1),((q /. (len q)) `2)]|)) \/ (LSeg (|[(p `1),((q /. (len q)) `2)]|,p)) is Element of K19( the carrier of (TOP-REAL 2))
L~ q is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
((LSeg ((q /. (len q)),|[(p `1),((q /. (len q)) `2)]|)) \/ (LSeg (|[(p `1),((q /. (len q)) `2)]|,p))) /\ (L~ q) is Element of K19( the carrier of (TOP-REAL 2))
{(q /. (len q))} is non empty set
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
union { (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
(L~ q) \/ (Ball (RR,RR)) is set
<*|[(p `1),((q /. (len q)) `2)]|*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q ^ <*|[(p `1),((q /. (len q)) `2)]|*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
<*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) ^ <*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
r9 is non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((q /. (len q)),|[(p `1),((q /. (len q)) `2)]|)) /\ (L~ q) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[(p `1),((q /. (len q)) `2)]|,p)) /\ (L~ q) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg ((q /. (len q)),|[(p `1),((q /. (len q)) `2)]|)) /\ (L~ q)) \/ ((LSeg (|[(p `1),((q /. (len q)) `2)]|,p)) /\ (L~ q)) is Element of K19( the carrier of (TOP-REAL 2))
len (q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
len <*|[(p `1),((q /. (len q)) `2)]|*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(len q) + (len <*|[(p `1),((q /. (len q)) `2)]|*>) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(len q) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) /. (len (q ^ <*|[(p `1),((q /. (len q)) `2)]|*>)) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
(q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ (q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg ((q ^ <*|[(p `1),((q /. (len q)) `2)]|*>),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) ) } is set
union { (LSeg ((q ^ <*|[(p `1),((q /. (len q)) `2)]|*>),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) ) } is set
(LSeg (|[(p `1),((q /. (len q)) `2)]|,p)) /\ (L~ (q ^ <*|[(p `1),((q /. (len q)) `2)]|*>)) is Element of K19( the carrier of (TOP-REAL 2))
{|[(p `1),((q /. (len q)) `2)]|} is non empty set
P2 is set
P2 is set
v is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q ^ <*|[(p `1),((q /. (len q)) `2)]|*>),v) is Element of K19( the carrier of (TOP-REAL 2))
v + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg ((q /. (len q)),|[(p `1),((q /. (len q)) `2)]|)) /\ (LSeg (|[(p `1),((q /. (len q)) `2)]|,p)) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,v) is Element of K19( the carrier of (TOP-REAL 2))
<*|[(p `1),((q /. (len q)) `2)]|*> ^ <*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q ^ (<*|[(p `1),((q /. (len q)) `2)]|*> ^ <*p*>) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
|[(p `1),((q /. (len q)) `2)]| `2 is ext-real V25() real Element of REAL
|[(p `1),((q /. (len q)) `2)]| `1 is ext-real V25() real Element of REAL
(L~ (q ^ <*|[(p `1),((q /. (len q)) `2)]|*>)) \/ (Ball (RR,RR)) is set
((L~ q) \/ (Ball (RR,RR))) \/ (Ball (RR,RR)) is set
(Ball (RR,RR)) \/ (Ball (RR,RR)) is Element of K19( the carrier of (Euclid 2))
(L~ q) \/ ((Ball (RR,RR)) \/ (Ball (RR,RR))) is set
x is non empty Element of K19( the carrier of (TOP-REAL 2))
(q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ ((q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) ^ <*p*>) is Element of K19( the carrier of (TOP-REAL 2))
len ((q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) ^ <*p*>) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (((q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) ^ <*p*>),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len ((q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) ^ <*p*>) ) } is set
union { (LSeg (((q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) ^ <*p*>),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len ((q ^ <*|[(p `1),((q /. (len q)) `2)]|*>) ^ <*p*>) ) } is set
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `2 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. (len q)) `1 is ext-real V25() real Element of REAL
|[((q /. (len q)) `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. (len q)) `2 is ext-real V25() real Element of REAL
<*|[((q /. (len q)) `1),(p `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q ^ <*|[((q /. (len q)) `1),(p `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg ((q /. (len q)),|[((q /. (len q)) `1),(p `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[((q /. (len q)) `1),(p `2)]|,p) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((q /. (len q)),|[((q /. (len q)) `1),(p `2)]|)) \/ (LSeg (|[((q /. (len q)) `1),(p `2)]|,p)) is Element of K19( the carrier of (TOP-REAL 2))
L~ q is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
((LSeg ((q /. (len q)),|[((q /. (len q)) `1),(p `2)]|)) \/ (LSeg (|[((q /. (len q)) `1),(p `2)]|,p))) /\ (L~ q) is Element of K19( the carrier of (TOP-REAL 2))
{(q /. (len q))} is non empty set
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
union { (LSeg (R,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
(L~ q) \/ (Ball (RR,RR)) is set
<*|[((q /. (len q)) `1),(p `2)]|*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q ^ <*|[((q /. (len q)) `1),(p `2)]|*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
<*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) ^ <*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
r9 is non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((q /. (len q)),|[((q /. (len q)) `1),(p `2)]|)) /\ (L~ q) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[((q /. (len q)) `1),(p `2)]|,p)) /\ (L~ q) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg ((q /. (len q)),|[((q /. (len q)) `1),(p `2)]|)) /\ (L~ q)) \/ ((LSeg (|[((q /. (len q)) `1),(p `2)]|,p)) /\ (L~ q)) is Element of K19( the carrier of (TOP-REAL 2))
len (q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
len <*|[((q /. (len q)) `1),(p `2)]|*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(len q) + (len <*|[((q /. (len q)) `1),(p `2)]|*>) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(len q) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) /. (len (q ^ <*|[((q /. (len q)) `1),(p `2)]|*>)) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
(q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ (q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg ((q ^ <*|[((q /. (len q)) `1),(p `2)]|*>),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) ) } is set
union { (LSeg ((q ^ <*|[((q /. (len q)) `1),(p `2)]|*>),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) ) } is set
(LSeg (|[((q /. (len q)) `1),(p `2)]|,p)) /\ (L~ (q ^ <*|[((q /. (len q)) `1),(p `2)]|*>)) is Element of K19( the carrier of (TOP-REAL 2))
{|[((q /. (len q)) `1),(p `2)]|} is non empty set
P2 is set
P2 is set
v is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q ^ <*|[((q /. (len q)) `1),(p `2)]|*>),v) is Element of K19( the carrier of (TOP-REAL 2))
v + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg ((q /. (len q)),|[((q /. (len q)) `1),(p `2)]|)) /\ (LSeg (|[((q /. (len q)) `1),(p `2)]|,p)) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,v) is Element of K19( the carrier of (TOP-REAL 2))
<*|[((q /. (len q)) `1),(p `2)]|*> ^ <*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q ^ (<*|[((q /. (len q)) `1),(p `2)]|*> ^ <*p*>) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
|[((q /. (len q)) `1),(p `2)]| `2 is ext-real V25() real Element of REAL
|[((q /. (len q)) `1),(p `2)]| `1 is ext-real V25() real Element of REAL
(L~ (q ^ <*|[((q /. (len q)) `1),(p `2)]|*>)) \/ (Ball (RR,RR)) is set
((L~ q) \/ (Ball (RR,RR))) \/ (Ball (RR,RR)) is set
(Ball (RR,RR)) \/ (Ball (RR,RR)) is Element of K19( the carrier of (Euclid 2))
(L~ q) \/ ((Ball (RR,RR)) \/ (Ball (RR,RR))) is set
x is non empty Element of K19( the carrier of (TOP-REAL 2))
(q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ ((q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) ^ <*p*>) is Element of K19( the carrier of (TOP-REAL 2))
len ((q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) ^ <*p*>) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (((q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) ^ <*p*>),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len ((q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) ^ <*p*>) ) } is set
union { (LSeg (((q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) ^ <*p*>),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len ((q ^ <*|[((q /. (len q)) `1),(p `2)]|*>) ^ <*p*>) ) } is set
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
R is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,R) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
(L~ q) \/ (Ball (RR,R)) is set
(len q) - 1 is ext-real V25() real Element of REAL
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P12 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P12 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,P12) is Element of K19( the carrier of (TOP-REAL 2))
R9 is ext-real non negative ordinal natural V25() real set
LSeg (q,R9) is Element of K19( the carrier of (TOP-REAL 2))
q2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. q2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (q2 + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
r is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
r9 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (q,q2) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,q2)) /\ (Ball (RR,R)) is Element of K19( the carrier of (Euclid 2))
LSeg (r,r9) is Element of K19( the carrier of (TOP-REAL 2))
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q | q2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (q | q2) is Element of K19( the carrier of (TOP-REAL 2))
len (q | q2) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((q | q2),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | q2) ) } is set
union { (LSeg ((q | q2),b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (q | q2) ) } is set
(Ball (RR,R)) /\ (L~ (q | q2)) is Element of K19( the carrier of (TOP-REAL 2))
the Element of (Ball (RR,R)) /\ (L~ (q | q2)) is Element of (Ball (RR,R)) /\ (L~ (q | q2))
Seg (len (q | q2)) is V33() V40( len (q | q2)) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (q | q2) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
P2 is set
P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | q2),P2) is Element of K19( the carrier of (TOP-REAL 2))
P2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,P2) is Element of K19( the carrier of (TOP-REAL 2))
Seg q2 is V33() V40(q2) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
(dom q) /\ (Seg q2) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q | (Seg q2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
dom (q | (Seg q2)) is set
(P2 + 1) - 1 is ext-real V25() real Element of REAL
(len (q | q2)) - 1 is ext-real V25() real Element of REAL
q2 - 1 is ext-real V25() real Element of REAL
- 1 is ext-real non positive V25() real Element of REAL
q2 + (- 1) is ext-real V25() real Element of REAL
(q2 + (- 1)) - q2 is ext-real V25() real Element of REAL
x is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,x) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,x)) /\ (Ball (RR,R)) is Element of K19( the carrier of (Euclid 2))
r `1 is ext-real V25() real Element of REAL
r `2 is ext-real V25() real Element of REAL
|[(r `1),(r `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
r9 `1 is ext-real V25() real Element of REAL
r9 `2 is ext-real V25() real Element of REAL
|[(r9 `1),(r9 `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
LSeg (q,p) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (r,q) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (q | q2)) \/ (LSeg (r,q)) is Element of K19( the carrier of (TOP-REAL 2))
P2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P2 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P2 /. (len P2) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P2 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P2,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P2 ) } is set
union { (LSeg (P2,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P2 ) } is set
<*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P2 ^ <*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(L~ P2) \/ (Ball (RR,R)) is set
(LSeg (q,p)) /\ (L~ P2) is Element of K19( the carrier of (TOP-REAL 2))
{q} is non empty set
(LSeg (q,p)) /\ (Ball (RR,R)) is Element of K19( the carrier of (Euclid 2))
(LSeg (q,p)) /\ ((L~ (q | q2)) \/ (LSeg (r,q))) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (q,p)) /\ (Ball (RR,R))) /\ (L~ (q | q2)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,p)) /\ (LSeg (r,q)) is Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (q,p)) /\ (Ball (RR,R))) /\ (L~ (q | q2))) \/ ((LSeg (q,p)) /\ (LSeg (r,q))) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,p)) /\ ((Ball (RR,R)) /\ (L~ (q | q2))) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (q,p)) /\ ((Ball (RR,R)) /\ (L~ (q | q2)))) \/ ((LSeg (q,p)) /\ (LSeg (r,q))) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (r,q)) /\ (LSeg (q,p)) is Element of K19( the carrier of (TOP-REAL 2))
v is set
P2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ P2 is Element of K19( the carrier of (TOP-REAL 2))
len P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (P2,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P2 ) } is set
union { (LSeg (P2,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P2 ) } is set
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
the Element of (LSeg (q,q2)) /\ (Ball (RR,R)) is Element of (LSeg (q,q2)) /\ (Ball (RR,R))
P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P2 `1 is ext-real V25() real Element of REAL
P2 `2 is ext-real V25() real Element of REAL
LSeg (r,P2) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (q | q2)) \/ (LSeg (r,P2)) is Element of K19( the carrier of (TOP-REAL 2))
P2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P2 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P2 /. (len P2) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ P2 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (P2,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P2 ) } is set
union { (LSeg (P2,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P2 ) } is set
|[(P2 `1),(P2 `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(P2 `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (P2,|[(P2 `1),(p `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(P2 `1),(p `2)]|,p) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ (L~ P2) is Element of K19( the carrier of (TOP-REAL 2))
{P2} is non empty set
g is set
((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ (Ball (RR,R)) is Element of K19( the carrier of (Euclid 2))
((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ ((L~ (q | q2)) \/ (LSeg (r,P2))) is Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ (Ball (RR,R))) /\ (L~ (q | q2)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ (LSeg (r,P2)) is Element of K19( the carrier of (TOP-REAL 2))
((((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ (Ball (RR,R))) /\ (L~ (q | q2))) \/ (((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ (LSeg (r,P2))) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ ((Ball (RR,R)) /\ (L~ (q | q2))) is Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ ((Ball (RR,R)) /\ (L~ (q | q2)))) \/ (((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ (LSeg (r,P2))) is Element of K19( the carrier of (TOP-REAL 2))
{} \/ (((LSeg (P2,|[(P2 `1),(p `2)]|)) \/ (LSeg (|[(P2 `1),(p `2)]|,p))) /\ (LSeg (r,P2))) is set
|[(P2 `1),(p `2)]| `2 is ext-real V25() real Element of REAL
<*|[(P2 `1),(p `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P2 ^ <*|[(P2 `1),(p `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(L~ P2) \/ (Ball (RR,R)) is set
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ g is Element of K19( the carrier of (TOP-REAL 2))
len g is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (g,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g ) } is set
union { (LSeg (g,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g ) } is set
|[(p `1),(P2 `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (P2,|[(p `1),(P2 `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(p `1),(P2 `2)]|,p) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ (L~ P2) is Element of K19( the carrier of (TOP-REAL 2))
{P2} is non empty set
g is set
((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ (Ball (RR,R)) is Element of K19( the carrier of (Euclid 2))
((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ ((L~ (q | q2)) \/ (LSeg (r,P2))) is Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ (Ball (RR,R))) /\ (L~ (q | q2)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ (LSeg (r,P2)) is Element of K19( the carrier of (TOP-REAL 2))
((((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ (Ball (RR,R))) /\ (L~ (q | q2))) \/ (((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ (LSeg (r,P2))) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ ((Ball (RR,R)) /\ (L~ (q | q2))) is Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ ((Ball (RR,R)) /\ (L~ (q | q2)))) \/ (((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ (LSeg (r,P2))) is Element of K19( the carrier of (TOP-REAL 2))
{} \/ (((LSeg (P2,|[(p `1),(P2 `2)]|)) \/ (LSeg (|[(p `1),(P2 `2)]|,p))) /\ (LSeg (r,P2))) is set
|[(p `1),(P2 `2)]| `1 is ext-real V25() real Element of REAL
<*|[(p `1),(P2 `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P2 ^ <*|[(p `1),(P2 `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(L~ P2) \/ (Ball (RR,R)) is set
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ g is Element of K19( the carrier of (TOP-REAL 2))
len g is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (g,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g ) } is set
union { (LSeg (g,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g ) } is set
|[(P2 `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(p `1),(P2 `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
v is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ v is Element of K19( the carrier of (TOP-REAL 2))
len v is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (v,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len v ) } is set
union { (LSeg (v,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len v ) } is set
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
union { (LSeg (q,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q ) } is set
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is ext-real V25() real Element of REAL
P12 is Element of the carrier of (Euclid 2)
Ball (P12,P11) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
R9 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ R9 is Element of K19( the carrier of (TOP-REAL 2))
len R9 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (R9,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R9 ) } is set
union { (LSeg (R9,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len R9 ) } is set
R9 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R9 /. (len R9) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q2 is Element of K19( the carrier of (TOP-REAL 2))
r is Element of K19( the carrier of (TOP-REAL 2))
r9 is Element of K19( the carrier of (TOP-REAL 2))
q2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q2 /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len q2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q2 /. (len q2) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ q2 is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (q2,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q2 ) } is set
union { (LSeg (q2,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q2 ) } is set
r is Element of K19( the carrier of (TOP-REAL 2))
r9 is Element of K19( the carrier of (TOP-REAL 2))
(L~ R9) \/ (Ball (P12,P11)) is set
q2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ q2 is Element of K19( the carrier of (TOP-REAL 2))
len q2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (q2,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q2 ) } is set
union { (LSeg (q2,b1)) where b1 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b1 & b1 + 1 <= len q2 ) } is set
r is Element of K19( the carrier of (TOP-REAL 2))
r9 is Element of K19( the carrier of (TOP-REAL 2))
q2 is Element of K19( the carrier of (TOP-REAL 2))
q2 is Element of K19( the carrier of (TOP-REAL 2))
TopSpaceMetr (Euclid 2) is TopStruct
the topology of (TOP-REAL 2) is non empty Element of K19(K19( the carrier of (TOP-REAL 2)))
K19(K19( the carrier of (TOP-REAL 2))) is set
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct
p is Element of K19( the carrier of (TOP-REAL 2))
q is Element of K19( the carrier of (TOP-REAL 2))
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( not b1 = R & b1 in p & ( for b2 being Element of K19( the carrier of (TOP-REAL 2)) holds
( not (b2,R,b1) or not b2 c= p ) ) ) } is set
the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty set
K19( the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)) is set
RR is Element of K19( the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #))
P11 is Element of the carrier of (Euclid 2)
R9 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R9 is ext-real V25() real set
Ball (P11,R9) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
q2 is ext-real V25() real set
P12 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
r is ext-real V25() real Element of REAL
Ball (P11,r) is Element of K19( the carrier of (Euclid 2))
Ball (P11,q2) is Element of K19( the carrier of (Euclid 2))
r9 is set
x is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P2 is Element of K19( the carrier of (TOP-REAL 2))
x is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P2 is Element of K19( the carrier of (TOP-REAL 2))
x is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Element of K19( the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b1 = p or ex b2 being Element of K19( the carrier of (TOP-REAL 2)) st
( (b2,p,b1) & b2 c= q ) ) } is set
R is Element of K19( the carrier of (TOP-REAL 2))
the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty set
K19( the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)) is set
RR is Element of K19( the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #))
P11 is Element of the carrier of (Euclid 2)
R9 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P12 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q2 is Element of K19( the carrier of (TOP-REAL 2))
q2 is Element of K19( the carrier of (TOP-REAL 2))
P12 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q2 is Element of K19( the carrier of (TOP-REAL 2))
P12 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P12 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q2 is ext-real V25() real set
Ball (P11,q2) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
r is ext-real V25() real set
r9 is ext-real V25() real Element of REAL
Ball (P11,r9) is Element of K19( the carrier of (Euclid 2))
Ball (P11,r) is Element of K19( the carrier of (Euclid 2))
x is set
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P2 is Element of K19( the carrier of (TOP-REAL 2))
P2 is Element of K19( the carrier of (TOP-REAL 2))
P2 is Element of K19( the carrier of (TOP-REAL 2))
P2 is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Element of K19( the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b1 = p or ex b2 being Element of K19( the carrier of (TOP-REAL 2)) st
( (b2,p,b1) & b2 c= q ) ) } is set
R is Element of K19( the carrier of (TOP-REAL 2))
RR is set
RR is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P11 is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b1 = p or ex b2 being Element of K19( the carrier of (TOP-REAL 2)) st
( (b2,p,b1) & b2 c= q ) ) } is set
R is Element of K19( the carrier of (TOP-REAL 2))
q \ R is Element of K19( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | q is strict TopSpace-like SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | q) is non proper closed Element of K19( the carrier of ((TOP-REAL 2) | q))
the carrier of ((TOP-REAL 2) | q) is set
K19( the carrier of ((TOP-REAL 2) | q)) is set
RR is Element of K19( the carrier of (TOP-REAL 2))
R \/ (q \ R) is Element of K19( the carrier of (TOP-REAL 2))
R \/ q is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of ((TOP-REAL 2) | q))
P12 is Element of K19( the carrier of ((TOP-REAL 2) | q))
P11 \/ P12 is Element of K19( the carrier of ((TOP-REAL 2) | q))
R9 is set
q2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
r is Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( not b1 = p & b1 in q & ( for b2 being Element of K19( the carrier of (TOP-REAL 2)) holds
( not (b2,p,b1) or not b2 c= q ) ) ) } is set
q2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
r is Element of K19( the carrier of (TOP-REAL 2))
r9 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R9 is non empty Element of K19( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | R9 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
R /\ ([#] ((TOP-REAL 2) | q)) is Element of K19( the carrier of ((TOP-REAL 2) | q))
the topology of ((TOP-REAL 2) | q) is non empty Element of K19(K19( the carrier of ((TOP-REAL 2) | q)))
K19(K19( the carrier of ((TOP-REAL 2) | q))) is set
RR /\ ([#] ((TOP-REAL 2) | q)) is Element of K19( the carrier of ((TOP-REAL 2) | q))
P11 /\ P12 is Element of K19( the carrier of ((TOP-REAL 2) | q))
{} ((TOP-REAL 2) | q) is functional empty FinSequence-membered closed V140() V141() V142() V143() V144() V145() V146() Element of K19( the carrier of ((TOP-REAL 2) | q))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b1 = p or ex b2 being Element of K19( the carrier of (TOP-REAL 2)) st
( (b2,p,b1) & b2 c= q ) ) } is set
R is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b1 = p or ex b2 being Element of K19( the carrier of (TOP-REAL 2)) st
( (b2,p,b1) & b2 c= R ) ) } is set
RR is set
P11 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P12 is Element of K19( the carrier of (TOP-REAL 2))
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
P12 is Element of K19( the carrier of (TOP-REAL 2))