:: JORDAN1 semantic presentation

REAL is V163() V164() V165() V169() set

NAT is V163() V164() V165() V166() V167() V168() V169() Element of K6(REAL)

K6(REAL) is non empty set

COMPLEX is V163() V169() set

omega is V163() V164() V165() V166() V167() V168() V169() set

K6(omega) is non empty set

I[01] is non empty strict TopSpace-like TopStruct

the carrier of I[01] is non empty set

1 is non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() Element of NAT

K7(1,1) is non empty set

K6(K7(1,1)) is non empty set

K7(K7(1,1),1) is non empty set

K6(K7(K7(1,1),1)) is non empty set

K7(K7(1,1),REAL) is set

K6(K7(K7(1,1),REAL)) is non empty set

K7(REAL,REAL) is set

K7(K7(REAL,REAL),REAL) is set

K6(K7(K7(REAL,REAL),REAL)) is non empty set

2 is non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() Element of NAT

K7(2,2) is non empty set

K7(K7(2,2),REAL) is set

K6(K7(K7(2,2),REAL)) is non empty set

RealSpace is strict MetrStruct

K263() is TopSpace-like TopStruct

K6(NAT) is non empty set

RAT is V163() V164() V165() V166() V169() set

INT is V163() V164() V165() V166() V167() V169() set

K6(K7(REAL,REAL)) is non empty set

TOP-REAL 2 is non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RLTopStruct

the carrier of (TOP-REAL 2) is non empty set

K6( the carrier of (TOP-REAL 2)) is non empty set

K7(COMPLEX,COMPLEX) is set

K6(K7(COMPLEX,COMPLEX)) is non empty set

K7(K7(COMPLEX,COMPLEX),COMPLEX) is set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set

K7(RAT,RAT) is set

K6(K7(RAT,RAT)) is non empty set

K7(K7(RAT,RAT),RAT) is set

K6(K7(K7(RAT,RAT),RAT)) is non empty set

K7(INT,INT) is set

K6(K7(INT,INT)) is non empty set

K7(K7(INT,INT),INT) is set

K6(K7(K7(INT,INT),INT)) is non empty set

K7(NAT,NAT) is set

K7(K7(NAT,NAT),NAT) is set

K6(K7(K7(NAT,NAT),NAT)) is non empty set

{} is empty V163() V164() V165() V166() V167() V168() V169() set

the empty V163() V164() V165() V166() V167() V168() V169() set is empty V163() V164() V165() V166() V167() V168() V169() set

0 is empty natural V11() real ext-real V115() V116() V163() V164() V165() V166() V167() V168() V169() Element of NAT

[.0,1.] is V163() V164() V165() Element of K6(REAL)

K265() is non empty strict TopSpace-like SubSpace of K263()

the carrier of K265() is non empty set

Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct

REAL 2 is non empty V114() M18( REAL )

K383(2,REAL) is V114() M18( REAL )

Pitag_dist 2 is V22() V25(K7((REAL 2),(REAL 2))) V26( REAL ) Function-like V33(K7((REAL 2),(REAL 2)), REAL ) Element of K6(K7(K7((REAL 2),(REAL 2)),REAL))

K7((REAL 2),(REAL 2)) is non empty set

K7(K7((REAL 2),(REAL 2)),REAL) is set

K6(K7(K7((REAL 2),(REAL 2)),REAL)) is non empty set

MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct

the carrier of (Euclid 2) is non empty set

{ b

p is non empty TopSpace-like TopStruct

the carrier of p is non empty set

K7( the carrier of I[01], the carrier of p) is non empty set

K6(K7( the carrier of I[01], the carrier of p)) is non empty set

y0 is Element of the carrier of p

P is Element of the carrier of p

w1 is V22() V25( the carrier of I[01]) V26( the carrier of p) Function-like V33( the carrier of I[01], the carrier of p) Element of K6(K7( the carrier of I[01], the carrier of p))

w1 . 0 is set

w1 . 1 is set

dom w1 is Element of K6( the carrier of I[01])

K6( the carrier of I[01]) is non empty set

rng w1 is Element of K6( the carrier of p)

K6( the carrier of p) is non empty set

w1 is non empty TopSpace-like TopStruct

the carrier of w1 is non empty set

K7( the carrier of w1, the carrier of p) is non empty set

K6(K7( the carrier of w1, the carrier of p)) is non empty set

w2 is V22() V25( the carrier of w1) V26( the carrier of p) Function-like V33( the carrier of w1, the carrier of p) Element of K6(K7( the carrier of w1, the carrier of p))

rng w2 is Element of K6( the carrier of p)

p is non empty TopSpace-like TopStruct

the carrier of p is non empty set

K6( the carrier of p) is non empty set

y0 is Element of K6( the carrier of p)

p | y0 is strict TopSpace-like SubSpace of p

the carrier of (p | y0) is set

K7( the carrier of I[01], the carrier of (p | y0)) is set

K6(K7( the carrier of I[01], the carrier of (p | y0))) is non empty set

P is non empty Element of K6( the carrier of p)

p | P is non empty strict TopSpace-like SubSpace of p

the carrier of (p | P) is non empty set

K7( the carrier of I[01], the carrier of (p | P)) is non empty set

K6(K7( the carrier of I[01], the carrier of (p | P))) is non empty set

w1 is Element of the carrier of p

w2 is Element of the carrier of p

x1 is Element of the carrier of (p | P)

I[01] --> x1 is V22() V25( the carrier of I[01]) V26( the carrier of (p | P)) Function-like V33( the carrier of I[01], the carrier of (p | P)) continuous Element of K6(K7( the carrier of I[01], the carrier of (p | P)))

K431( the carrier of (p | P), the carrier of I[01],x1) is V22() V25( the carrier of I[01]) V26( the carrier of (p | P)) Function-like V33( the carrier of I[01], the carrier of (p | P)) Element of K6(K7( the carrier of I[01], the carrier of (p | P)))

x2 is V22() V25( the carrier of I[01]) V26( the carrier of (p | P)) Function-like V33( the carrier of I[01], the carrier of (p | P)) Element of K6(K7( the carrier of I[01], the carrier of (p | P)))

x2 . 0 is set

x2 . 1 is set

w1 is Element of the carrier of (p | P)

w2 is Element of the carrier of (p | P)

[#] (p | P) is non empty non proper closed Element of K6( the carrier of (p | P))

K6( the carrier of (p | P)) is non empty set

K6( the carrier of (p | y0)) is non empty set

[#] (p | y0) is non proper closed Element of K6( the carrier of (p | y0))

w1 is Element of K6( the carrier of (p | y0))

w2 is Element of K6( the carrier of (p | y0))

w1 \/ w2 is Element of K6( the carrier of (p | y0))

{} (p | y0) is empty closed V163() V164() V165() V166() V167() V168() V169() Element of K6( the carrier of (p | y0))

P is empty proper closed V163() V164() V165() V166() V167() V168() V169() Element of K6( the carrier of p)

p | P is empty V50() V51() {} -element strict TopSpace-like T_0 SubSpace of p

[#] (p | P) is empty V2() non proper closed V163() V164() V165() V166() V167() V168() V169() Element of K6( the carrier of (p | P))

the carrier of (p | P) is empty V2() V36() V163() V164() V165() V166() V167() V168() V169() set

K6( the carrier of (p | P)) is non empty set

p is non empty TopSpace-like TopStruct

the carrier of p is non empty set

K6( the carrier of p) is non empty set

y0 is Element of K6( the carrier of p)

P is Element of K6( the carrier of p)

y0 \/ P is Element of K6( the carrier of p)

p is non empty TopSpace-like TopStruct

the carrier of p is non empty set

K6( the carrier of p) is non empty set

y0 is Element of K6( the carrier of p)

P is Element of K6( the carrier of p)

w1 is Element of K6( the carrier of p)

y0 \/ P is Element of K6( the carrier of p)

(y0 \/ P) \/ w1 is Element of K6( the carrier of p)

P /\ w1 is Element of K6( the carrier of p)

(y0 \/ P) /\ w1 is Element of K6( the carrier of p)

y0 /\ w1 is Element of K6( the carrier of p)

(y0 /\ w1) \/ (P /\ w1) is Element of K6( the carrier of p)

p is non empty TopSpace-like TopStruct

the carrier of p is non empty set

K6( the carrier of p) is non empty set

y0 is Element of K6( the carrier of p)

P is Element of K6( the carrier of p)

w1 is Element of K6( the carrier of p)

w2 is Element of K6( the carrier of p)

y0 \/ P is Element of K6( the carrier of p)

(y0 \/ P) \/ w1 is Element of K6( the carrier of p)

((y0 \/ P) \/ w1) \/ w2 is Element of K6( the carrier of p)

w1 /\ w2 is Element of K6( the carrier of p)

((y0 \/ P) \/ w1) /\ w2 is Element of K6( the carrier of p)

(y0 \/ P) /\ w2 is Element of K6( the carrier of p)

((y0 \/ P) /\ w2) \/ (w1 /\ w2) is Element of K6( the carrier of p)

p is non empty V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of p is non empty set

K6( the carrier of p) is non empty set

y0 is Element of K6( the carrier of p)

P is Element of the carrier of p

w1 is Element of the carrier of p

LSeg (P,w1) is non empty convex Element of K6( the carrier of p)

{ (((1 - b

p is natural V11() real ext-real set

TOP-REAL p is non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RLTopStruct

the carrier of (TOP-REAL p) is non empty set

K6( the carrier of (TOP-REAL p)) is non empty set

y0 is Element of K6( the carrier of (TOP-REAL p))

(TOP-REAL p) | y0 is strict TopSpace-like SubSpace of TOP-REAL p

the carrier of ((TOP-REAL p) | y0) is set

K7( the carrier of I[01], the carrier of ((TOP-REAL p) | y0)) is set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL p) | y0))) is non empty set

P is V43(p) V112() V155() Element of the carrier of (TOP-REAL p)

w1 is V43(p) V112() V155() Element of the carrier of (TOP-REAL p)

LSeg (P,w1) is non empty convex Element of K6( the carrier of (TOP-REAL p))

{ (((1 - b

(TOP-REAL p) | (LSeg (P,w1)) is non empty strict TopSpace-like SubSpace of TOP-REAL p

the carrier of ((TOP-REAL p) | (LSeg (P,w1))) is non empty set

K7( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (P,w1)))) is non empty set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (P,w1))))) is non empty set

w2 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL p) | (LSeg (P,w1)))) Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (P,w1)))) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (P,w1)))))

w2 . 0 is set

w2 . 1 is set

rng w2 is Element of K6( the carrier of ((TOP-REAL p) | (LSeg (P,w1))))

K6( the carrier of ((TOP-REAL p) | (LSeg (P,w1)))) is non empty set

[#] ((TOP-REAL p) | (LSeg (P,w1))) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL p) | (LSeg (P,w1))))

[#] ((TOP-REAL p) | y0) is non proper closed Element of K6( the carrier of ((TOP-REAL p) | y0))

K6( the carrier of ((TOP-REAL p) | y0)) is non empty set

dom w2 is Element of K6( the carrier of I[01])

K6( the carrier of I[01]) is non empty set

K7([.0,1.],y0) is set

K6(K7([.0,1.],y0)) is non empty set

x1 is V22() V25([.0,1.]) V26(y0) Function-like V33([.0,1.],y0) Element of K6(K7([.0,1.],y0))

x2 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL p) | y0)) Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL p) | y0)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL p) | y0)))

K6((REAL 2)) is non empty set

p is V11() real ext-real Element of REAL

{ |[b

y0 is set

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

|[P,w1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

{ |[b

y0 is set

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

|[P,w1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

{ |[b

y0 is set

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

|[P,w1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

{ |[b

y0 is set

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

|[P,w1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ |[b

w2 is set

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ |[b

w2 is set

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

{ |[b

y0 is V11() real ext-real Element of REAL

{ |[b

{ |[b

P is V11() real ext-real Element of REAL

{ |[b

( { |[b

w1 is V11() real ext-real Element of REAL

{ |[b

{ |[b

(( { |[b

w2 is set

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w2 is set

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v1 is V11() real ext-real Element of REAL

l is V11() real ext-real Element of REAL

|[v1,l]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v `1 is V11() real ext-real Element of REAL

v `2 is V11() real ext-real Element of REAL

v1 is V11() real ext-real Element of REAL

l is V11() real ext-real Element of REAL

|[v1,l]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v1 is V11() real ext-real Element of REAL

l is V11() real ext-real Element of REAL

|[v1,l]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v1 is V11() real ext-real Element of REAL

l is V11() real ext-real Element of REAL

|[v1,l]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

{ |[b

y0 is V11() real ext-real Element of REAL

{ |[b

P is V11() real ext-real Element of REAL

{ |[b

{ |[b

( { |[b

w1 is V11() real ext-real Element of REAL

{ |[b

{ |[b

(( { |[b

w2 is set

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w2 is set

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v is V11() real ext-real Element of REAL

v1 is V11() real ext-real Element of REAL

|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l is V11() real ext-real Element of REAL

q is V11() real ext-real Element of REAL

|[l,q]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

Q is V11() real ext-real Element of REAL

QQ is V11() real ext-real Element of REAL

|[Q,QQ]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ |[b

w2 is Element of K6( the carrier of (TOP-REAL 2))

x1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

LSeg (x1,x2) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

v is set

v1 is V11() real ext-real Element of REAL

l is V11() real ext-real Element of REAL

|[v1,l]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x1 `1 is V11() real ext-real Element of REAL

x1 `2 is V11() real ext-real Element of REAL

q is V11() real ext-real Element of REAL

Q is V11() real ext-real Element of REAL

|[q,Q]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x2 `1 is V11() real ext-real Element of REAL

x2 `2 is V11() real ext-real Element of REAL

QQ is V11() real ext-real Element of REAL

1 - QQ is V11() real ext-real Element of REAL

(1 - QQ) * x1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

QQ * x2 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

((1 - QQ) * x1) + (QQ * x2) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

((1 - QQ) * x1) `1 is V11() real ext-real Element of REAL

(QQ * x2) `1 is V11() real ext-real Element of REAL

(((1 - QQ) * x1) `1) + ((QQ * x2) `1) is V11() real ext-real Element of REAL

((1 - QQ) * x1) `2 is V11() real ext-real Element of REAL

(QQ * x2) `2 is V11() real ext-real Element of REAL

(((1 - QQ) * x1) `2) + ((QQ * x2) `2) is V11() real ext-real Element of REAL

|[((((1 - QQ) * x1) `1) + ((QQ * x2) `1)),((((1 - QQ) * x1) `2) + ((QQ * x2) `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

(1 - QQ) * (x1 `1) is V11() real ext-real Element of REAL

(1 - QQ) * (x1 `2) is V11() real ext-real Element of REAL

|[((1 - QQ) * (x1 `1)),((1 - QQ) * (x1 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

QQ * (x2 `1) is V11() real ext-real Element of REAL

QQ * (x2 `2) is V11() real ext-real Element of REAL

|[(QQ * (x2 `1)),(QQ * (x2 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

(((1 - QQ) * x1) + (QQ * x2)) `1 is V11() real ext-real Element of REAL

((1 - QQ) * (x1 `1)) + (QQ * (x2 `1)) is V11() real ext-real Element of REAL

(((1 - QQ) * x1) + (QQ * x2)) `2 is V11() real ext-real Element of REAL

((1 - QQ) * (x1 `2)) + (QQ * (x2 `2)) is V11() real ext-real Element of REAL

|[((((1 - QQ) * x1) + (QQ * x2)) `1),((((1 - QQ) * x1) + (QQ * x2)) `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

{ |[b

y0 is Element of K6( the carrier of (TOP-REAL 2))

P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

LSeg (P,w1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

w2 is set

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

P `1 is V11() real ext-real Element of REAL

v is V11() real ext-real Element of REAL

v1 is V11() real ext-real Element of REAL

|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w1 `1 is V11() real ext-real Element of REAL

l is V11() real ext-real Element of REAL

1 - l is V11() real ext-real Element of REAL

(1 - l) * P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

((1 - l) * P) + (l * w1) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

((1 - l) * P) `1 is V11() real ext-real Element of REAL

(l * w1) `1 is V11() real ext-real Element of REAL

(((1 - l) * P) `1) + ((l * w1) `1) is V11() real ext-real Element of REAL

((1 - l) * P) `2 is V11() real ext-real Element of REAL

(l * w1) `2 is V11() real ext-real Element of REAL

(((1 - l) * P) `2) + ((l * w1) `2) is V11() real ext-real Element of REAL

|[((((1 - l) * P) `1) + ((l * w1) `1)),((((1 - l) * P) `2) + ((l * w1) `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

(1 - l) * (P `1) is V11() real ext-real Element of REAL

P `2 is V11() real ext-real Element of REAL

(1 - l) * (P `2) is V11() real ext-real Element of REAL

|[((1 - l) * (P `1)),((1 - l) * (P `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l * (w1 `1) is V11() real ext-real Element of REAL

w1 `2 is V11() real ext-real Element of REAL

l * (w1 `2) is V11() real ext-real Element of REAL

|[(l * (w1 `1)),(l * (w1 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

(((1 - l) * P) + (l * w1)) `1 is V11() real ext-real Element of REAL

((1 - l) * (P `1)) + (l * (w1 `1)) is V11() real ext-real Element of REAL

(((1 - l) * P) + (l * w1)) `2 is V11() real ext-real Element of REAL

|[((((1 - l) * P) + (l * w1)) `1),((((1 - l) * P) + (l * w1)) `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

{ |[b

y0 is Element of K6( the carrier of (TOP-REAL 2))

P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

LSeg (P,w1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

w2 is set

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

P `1 is V11() real ext-real Element of REAL

v is V11() real ext-real Element of REAL

v1 is V11() real ext-real Element of REAL

|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w1 `1 is V11() real ext-real Element of REAL

l is V11() real ext-real Element of REAL

1 - l is V11() real ext-real Element of REAL

(1 - l) * P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

((1 - l) * P) + (l * w1) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

((1 - l) * P) `1 is V11() real ext-real Element of REAL

(l * w1) `1 is V11() real ext-real Element of REAL

(((1 - l) * P) `1) + ((l * w1) `1) is V11() real ext-real Element of REAL

((1 - l) * P) `2 is V11() real ext-real Element of REAL

(l * w1) `2 is V11() real ext-real Element of REAL

(((1 - l) * P) `2) + ((l * w1) `2) is V11() real ext-real Element of REAL

|[((((1 - l) * P) `1) + ((l * w1) `1)),((((1 - l) * P) `2) + ((l * w1) `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

(1 - l) * (P `1) is V11() real ext-real Element of REAL

P `2 is V11() real ext-real Element of REAL

(1 - l) * (P `2) is V11() real ext-real Element of REAL

|[((1 - l) * (P `1)),((1 - l) * (P `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l * (w1 `1) is V11() real ext-real Element of REAL

w1 `2 is V11() real ext-real Element of REAL

l * (w1 `2) is V11() real ext-real Element of REAL

|[(l * (w1 `1)),(l * (w1 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

(((1 - l) * P) + (l * w1)) `1 is V11() real ext-real Element of REAL

((1 - l) * (P `1)) + (l * (w1 `1)) is V11() real ext-real Element of REAL

(((1 - l) * P) + (l * w1)) `2 is V11() real ext-real Element of REAL

|[((((1 - l) * P) + (l * w1)) `1),((((1 - l) * P) + (l * w1)) `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

{ |[b

y0 is Element of K6( the carrier of (TOP-REAL 2))

P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

LSeg (P,w1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

w2 is set

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

P `2 is V11() real ext-real Element of REAL

v is V11() real ext-real Element of REAL

v1 is V11() real ext-real Element of REAL

|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w1 `2 is V11() real ext-real Element of REAL

l is V11() real ext-real Element of REAL

1 - l is V11() real ext-real Element of REAL

(1 - l) * P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

((1 - l) * P) + (l * w1) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

((1 - l) * P) `1 is V11() real ext-real Element of REAL

(l * w1) `1 is V11() real ext-real Element of REAL

(((1 - l) * P) `1) + ((l * w1) `1) is V11() real ext-real Element of REAL

((1 - l) * P) `2 is V11() real ext-real Element of REAL

(l * w1) `2 is V11() real ext-real Element of REAL

(((1 - l) * P) `2) + ((l * w1) `2) is V11() real ext-real Element of REAL

|[((((1 - l) * P) `1) + ((l * w1) `1)),((((1 - l) * P) `2) + ((l * w1) `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

P `1 is V11() real ext-real Element of REAL

(1 - l) * (P `1) is V11() real ext-real Element of REAL

(1 - l) * (P `2) is V11() real ext-real Element of REAL

|[((1 - l) * (P `1)),((1 - l) * (P `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w1 `1 is V11() real ext-real Element of REAL

l * (w1 `1) is V11() real ext-real Element of REAL

l * (w1 `2) is V11() real ext-real Element of REAL

|[(l * (w1 `1)),(l * (w1 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

(((1 - l) * P) + (l * w1)) `2 is V11() real ext-real Element of REAL

((1 - l) * (P `2)) + (l * (w1 `2)) is V11() real ext-real Element of REAL

(((1 - l) * P) + (l * w1)) `1 is V11() real ext-real Element of REAL

|[((((1 - l) * P) + (l * w1)) `1),((((1 - l) * P) + (l * w1)) `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

{ |[b

y0 is Element of K6( the carrier of (TOP-REAL 2))

P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

LSeg (P,w1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

w2 is set

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

P `2 is V11() real ext-real Element of REAL

v is V11() real ext-real Element of REAL

v1 is V11() real ext-real Element of REAL

|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w1 `2 is V11() real ext-real Element of REAL

l is V11() real ext-real Element of REAL

1 - l is V11() real ext-real Element of REAL

(1 - l) * P is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l * w1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

((1 - l) * P) + (l * w1) is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

((1 - l) * P) `1 is V11() real ext-real Element of REAL

(l * w1) `1 is V11() real ext-real Element of REAL

(((1 - l) * P) `1) + ((l * w1) `1) is V11() real ext-real Element of REAL

((1 - l) * P) `2 is V11() real ext-real Element of REAL

(l * w1) `2 is V11() real ext-real Element of REAL

(((1 - l) * P) `2) + ((l * w1) `2) is V11() real ext-real Element of REAL

|[((((1 - l) * P) `1) + ((l * w1) `1)),((((1 - l) * P) `2) + ((l * w1) `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

P `1 is V11() real ext-real Element of REAL

(1 - l) * (P `1) is V11() real ext-real Element of REAL

(1 - l) * (P `2) is V11() real ext-real Element of REAL

|[((1 - l) * (P `1)),((1 - l) * (P `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w1 `1 is V11() real ext-real Element of REAL

l * (w1 `1) is V11() real ext-real Element of REAL

l * (w1 `2) is V11() real ext-real Element of REAL

|[(l * (w1 `1)),(l * (w1 `2))]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

(((1 - l) * P) + (l * w1)) `2 is V11() real ext-real Element of REAL

((1 - l) * (P `2)) + (l * (w1 `2)) is V11() real ext-real Element of REAL

(((1 - l) * P) + (l * w1)) `1 is V11() real ext-real Element of REAL

|[((((1 - l) * P) + (l * w1)) `1),((((1 - l) * P) + (l * w1)) `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ |[b

w2 is Element of K6( the carrier of (TOP-REAL 2))

{ |[b

{ |[b

{ |[b

{ |[b

( { |[b

{ |[b

(( { |[b

p - 1 is V11() real ext-real Element of REAL

y0 - 1 is V11() real ext-real Element of REAL

|[(p - 1),(y0 - 1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x1 is Element of K6( the carrier of (TOP-REAL 2))

x2 is Element of K6( the carrier of (TOP-REAL 2))

x1 /\ x2 is Element of K6( the carrier of (TOP-REAL 2))

P + 1 is V11() real ext-real Element of REAL

|[(P + 1),(y0 - 1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v is Element of K6( the carrier of (TOP-REAL 2))

x2 /\ v is Element of K6( the carrier of (TOP-REAL 2))

w1 + 1 is V11() real ext-real Element of REAL

|[(P + 1),(w1 + 1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v1 is Element of K6( the carrier of (TOP-REAL 2))

v /\ v1 is Element of K6( the carrier of (TOP-REAL 2))

the topology of (TOP-REAL 2) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))

K6(K6( the carrier of (TOP-REAL 2))) is non empty set

TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct

TopSpaceMetr (Euclid 2) is TopStruct

Family_open_set (Euclid 2) is Element of K6(K6( the carrier of (Euclid 2)))

K6( the carrier of (Euclid 2)) is non empty set

K6(K6( the carrier of (Euclid 2))) is non empty set

TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #) is non empty strict TopStruct

p is V11() real ext-real Element of REAL

{ |[b

y0 is Element of K6( the carrier of (TOP-REAL 2))

the carrier of (TopSpaceMetr (Euclid 2)) is set

K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set

w1 is Element of the carrier of (Euclid 2)

w2 is V11() real ext-real Element of REAL

x1 is V11() real ext-real Element of REAL

|[w2,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

w2 - p is V11() real ext-real Element of REAL

(w2 - p) / 2 is V11() real ext-real Element of REAL

Ball (w1,((w2 - p) / 2)) is Element of K6( the carrier of (Euclid 2))

v is set

{ b

v1 is Element of the carrier of (Euclid 2)

dist (w1,v1) is V11() real ext-real Element of REAL

(Pitag_dist 2) . (w1,v1) is set

l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l `1 is V11() real ext-real Element of REAL

q is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

q `1 is V11() real ext-real Element of REAL

(l `1) - (q `1) is V11() real ext-real Element of REAL

((l `1) - (q `1)) ^2 is V11() real ext-real Element of REAL

K37(((l `1) - (q `1)),((l `1) - (q `1))) is V11() real ext-real set

l `2 is V11() real ext-real Element of REAL

q `2 is V11() real ext-real Element of REAL

(l `2) - (q `2) is V11() real ext-real Element of REAL

((l `2) - (q `2)) ^2 is V11() real ext-real Element of REAL

K37(((l `2) - (q `2)),((l `2) - (q `2))) is V11() real ext-real set

(((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)) is V11() real ext-real Element of REAL

0 + 0 is V11() real ext-real Element of REAL

((w2 - p) / 2) ^2 is V11() real ext-real Element of REAL

K37(((w2 - p) / 2),((w2 - p) / 2)) is V11() real ext-real set

(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))) ^2 is V11() real ext-real Element of REAL

K37((sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))),(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)))) is V11() real ext-real set

(q `1) + ((w2 - p) / 2) is V11() real ext-real Element of REAL

(l `1) - ((w2 - p) / 2) is V11() real ext-real Element of REAL

w2 - ((w2 - p) / 2) is V11() real ext-real Element of REAL

((w2 - p) / 2) + p is V11() real ext-real Element of REAL

|[(q `1),(q `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

P is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))

p is V11() real ext-real Element of REAL

{ |[b

y0 is Element of K6( the carrier of (TOP-REAL 2))

the carrier of (TopSpaceMetr (Euclid 2)) is set

K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set

w1 is Element of the carrier of (Euclid 2)

w2 is V11() real ext-real Element of REAL

x1 is V11() real ext-real Element of REAL

|[w2,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p - w2 is V11() real ext-real Element of REAL

(p - w2) / 2 is V11() real ext-real Element of REAL

Ball (w1,((p - w2) / 2)) is Element of K6( the carrier of (Euclid 2))

v is set

{ b

v1 is Element of the carrier of (Euclid 2)

dist (w1,v1) is V11() real ext-real Element of REAL

(Pitag_dist 2) . (w1,v1) is set

l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l `1 is V11() real ext-real Element of REAL

q is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

q `1 is V11() real ext-real Element of REAL

(l `1) - (q `1) is V11() real ext-real Element of REAL

((l `1) - (q `1)) ^2 is V11() real ext-real Element of REAL

K37(((l `1) - (q `1)),((l `1) - (q `1))) is V11() real ext-real set

l `2 is V11() real ext-real Element of REAL

q `2 is V11() real ext-real Element of REAL

(l `2) - (q `2) is V11() real ext-real Element of REAL

((l `2) - (q `2)) ^2 is V11() real ext-real Element of REAL

K37(((l `2) - (q `2)),((l `2) - (q `2))) is V11() real ext-real set

(((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)) is V11() real ext-real Element of REAL

0 + 0 is V11() real ext-real Element of REAL

((p - w2) / 2) ^2 is V11() real ext-real Element of REAL

K37(((p - w2) / 2),((p - w2) / 2)) is V11() real ext-real set

(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))) ^2 is V11() real ext-real Element of REAL

K37((sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))),(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)))) is V11() real ext-real set

(q `1) - (l `1) is V11() real ext-real Element of REAL

((q `1) - (l `1)) ^2 is V11() real ext-real Element of REAL

K37(((q `1) - (l `1)),((q `1) - (l `1))) is V11() real ext-real set

(l `1) + ((p - w2) / 2) is V11() real ext-real Element of REAL

w2 + ((p - w2) / 2) is V11() real ext-real Element of REAL

p - ((p - w2) / 2) is V11() real ext-real Element of REAL

|[(q `1),(q `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

P is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))

p is V11() real ext-real Element of REAL

{ |[b

y0 is Element of K6( the carrier of (TOP-REAL 2))

the carrier of (TopSpaceMetr (Euclid 2)) is set

K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set

w1 is Element of the carrier of (Euclid 2)

w2 is V11() real ext-real Element of REAL

x1 is V11() real ext-real Element of REAL

|[w2,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x1 - p is V11() real ext-real Element of REAL

(x1 - p) / 2 is V11() real ext-real Element of REAL

Ball (w1,((x1 - p) / 2)) is Element of K6( the carrier of (Euclid 2))

v is set

{ b

v1 is Element of the carrier of (Euclid 2)

dist (w1,v1) is V11() real ext-real Element of REAL

(Pitag_dist 2) . (w1,v1) is set

l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l `1 is V11() real ext-real Element of REAL

q is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

q `1 is V11() real ext-real Element of REAL

(l `1) - (q `1) is V11() real ext-real Element of REAL

((l `1) - (q `1)) ^2 is V11() real ext-real Element of REAL

K37(((l `1) - (q `1)),((l `1) - (q `1))) is V11() real ext-real set

l `2 is V11() real ext-real Element of REAL

q `2 is V11() real ext-real Element of REAL

(l `2) - (q `2) is V11() real ext-real Element of REAL

((l `2) - (q `2)) ^2 is V11() real ext-real Element of REAL

K37(((l `2) - (q `2)),((l `2) - (q `2))) is V11() real ext-real set

(((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)) is V11() real ext-real Element of REAL

0 + 0 is V11() real ext-real Element of REAL

((x1 - p) / 2) ^2 is V11() real ext-real Element of REAL

K37(((x1 - p) / 2),((x1 - p) / 2)) is V11() real ext-real set

(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))) ^2 is V11() real ext-real Element of REAL

K37((sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))),(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)))) is V11() real ext-real set

(((l `2) - (q `2)) ^2) + (((l `1) - (q `1)) ^2) is V11() real ext-real Element of REAL

(q `2) + ((x1 - p) / 2) is V11() real ext-real Element of REAL

(l `2) - ((x1 - p) / 2) is V11() real ext-real Element of REAL

x1 - ((x1 - p) / 2) is V11() real ext-real Element of REAL

((x1 - p) / 2) + p is V11() real ext-real Element of REAL

|[(q `1),(q `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

P is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))

p is V11() real ext-real Element of REAL

{ |[b

y0 is Element of K6( the carrier of (TOP-REAL 2))

the carrier of (TopSpaceMetr (Euclid 2)) is set

K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set

w1 is Element of the carrier of (Euclid 2)

w2 is V11() real ext-real Element of REAL

x1 is V11() real ext-real Element of REAL

|[w2,x1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p - x1 is V11() real ext-real Element of REAL

(p - x1) / 2 is V11() real ext-real Element of REAL

Ball (w1,((p - x1) / 2)) is Element of K6( the carrier of (Euclid 2))

v is set

{ b

v1 is Element of the carrier of (Euclid 2)

dist (w1,v1) is V11() real ext-real Element of REAL

(Pitag_dist 2) . (w1,v1) is set

l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l `1 is V11() real ext-real Element of REAL

q is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

q `1 is V11() real ext-real Element of REAL

(l `1) - (q `1) is V11() real ext-real Element of REAL

((l `1) - (q `1)) ^2 is V11() real ext-real Element of REAL

K37(((l `1) - (q `1)),((l `1) - (q `1))) is V11() real ext-real set

l `2 is V11() real ext-real Element of REAL

q `2 is V11() real ext-real Element of REAL

(l `2) - (q `2) is V11() real ext-real Element of REAL

((l `2) - (q `2)) ^2 is V11() real ext-real Element of REAL

K37(((l `2) - (q `2)),((l `2) - (q `2))) is V11() real ext-real set

(((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)) is V11() real ext-real Element of REAL

0 + 0 is V11() real ext-real Element of REAL

((p - x1) / 2) ^2 is V11() real ext-real Element of REAL

K37(((p - x1) / 2),((p - x1) / 2)) is V11() real ext-real set

(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))) ^2 is V11() real ext-real Element of REAL

K37((sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2))),(sqrt ((((l `1) - (q `1)) ^2) + (((l `2) - (q `2)) ^2)))) is V11() real ext-real set

(q `2) - (l `2) is V11() real ext-real Element of REAL

((q `2) - (l `2)) ^2 is V11() real ext-real Element of REAL

K37(((q `2) - (l `2)),((q `2) - (l `2))) is V11() real ext-real set

(l `2) + ((p - x1) / 2) is V11() real ext-real Element of REAL

x1 + ((p - x1) / 2) is V11() real ext-real Element of REAL

p - ((p - x1) / 2) is V11() real ext-real Element of REAL

|[(q `1),(q `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

P is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ |[b

w2 is Element of K6( the carrier of (TOP-REAL 2))

{ |[b

{ |[b

{ |[b

{ |[b

x1 is Element of K6( the carrier of (TOP-REAL 2))

x2 is Element of K6( the carrier of (TOP-REAL 2))

x1 /\ x2 is Element of K6( the carrier of (TOP-REAL 2))

v is Element of K6( the carrier of (TOP-REAL 2))

(x1 /\ x2) /\ v is Element of K6( the carrier of (TOP-REAL 2))

v1 is Element of K6( the carrier of (TOP-REAL 2))

((x1 /\ x2) /\ v) /\ v1 is Element of K6( the carrier of (TOP-REAL 2))

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ |[b

w2 is Element of K6( the carrier of (TOP-REAL 2))

{ |[b

{ |[b

{ |[b

{ |[b

( { |[b

{ |[b

(( { |[b

x1 is Element of K6( the carrier of (TOP-REAL 2))

x2 is Element of K6( the carrier of (TOP-REAL 2))

x1 \/ x2 is Element of K6( the carrier of (TOP-REAL 2))

v is Element of K6( the carrier of (TOP-REAL 2))

(x1 \/ x2) \/ v is Element of K6( the carrier of (TOP-REAL 2))

v1 is Element of K6( the carrier of (TOP-REAL 2))

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ |[b

{ |[b

w2 is Element of K6( the carrier of (TOP-REAL 2))

x1 is Element of K6( the carrier of (TOP-REAL 2))

x2 is set

v is V11() real ext-real Element of REAL

v1 is V11() real ext-real Element of REAL

|[v,v1]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

|[v,v1]| `1 is V11() real ext-real Element of REAL

|[v,v1]| `2 is V11() real ext-real Element of REAL

q is V11() real ext-real Element of REAL

Q is V11() real ext-real Element of REAL

|[q,Q]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ b

{ |[b

w2 is set

x1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x1 `1 is V11() real ext-real Element of REAL

x1 `2 is V11() real ext-real Element of REAL

|[(x1 `1),(x1 `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

|[x1,x2]| `1 is V11() real ext-real Element of REAL

|[x1,x2]| `2 is V11() real ext-real Element of REAL

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ b

{ |[b

w2 is set

x1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x1 `1 is V11() real ext-real Element of REAL

x1 `2 is V11() real ext-real Element of REAL

|[(x1 `1),(x1 `2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

x1 is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of REAL

|[x1,x2]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

|[x1,x2]| `1 is V11() real ext-real Element of REAL

|[x1,x2]| `2 is V11() real ext-real Element of REAL

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ b

{ |[b

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ b

{ |[b

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ b

w2 is Element of K6( the carrier of (TOP-REAL 2))

{ |[b

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ b

w2 is Element of K6( the carrier of (TOP-REAL 2))

{ |[b

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ b

w2 is Element of K6( the carrier of (TOP-REAL 2))

{ |[b

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ b

w2 is Element of K6( the carrier of (TOP-REAL 2))

{ |[b

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ b

{ b

w2 is Element of K6( the carrier of (TOP-REAL 2))

x1 is Element of K6( the carrier of (TOP-REAL 2))

{ |[b

{ |[b

p is V11() real ext-real Element of REAL

y0 is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

w1 is V11() real ext-real Element of REAL

{ b

{ b

{ b

w2 is Element of K6( the carrier of (TOP-REAL 2))

x1 is Element of K6( the carrier of (TOP-REAL 2))

x2 is Element of K6( the carrier of (TOP-REAL 2))

w2 ` is Element of K6( the carrier of (TOP-REAL 2))

the carrier of (TOP-REAL 2) \ w2 is set

x1 \/ x2 is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (w2 `) is strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | (w2 `)) is set

K6( the carrier of ((TOP-REAL 2) | (w2 `))) is non empty set

v is set

v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v1 `1 is V11() real ext-real Element of REAL

v1 `2 is V11() real ext-real Element of REAL

v is set

v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v1 `1 is V11() real ext-real Element of REAL

v1 `2 is V11() real ext-real Element of REAL

l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l `1 is V11() real ext-real Element of REAL

l `2 is V11() real ext-real Element of REAL

v1 is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

v1 `1 is V11() real ext-real Element of REAL

v1 `2 is V11() real ext-real Element of REAL

l is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

l `1 is V11() real ext-real Element of REAL

l `2 is V11() real ext-real Element of REAL

p + P is V11() real ext-real Element of REAL

(p + P) / 2 is V11() real ext-real Element of REAL

y0 + w1 is V11() real ext-real Element of REAL

(y0 + w1) / 2 is V11() real ext-real Element of REAL

p + p is V11() real ext-real Element of REAL

y0 + y0 is V11() real ext-real Element of REAL

(p + p) / 2 is V11() real ext-real Element of REAL

(y0 + y0) / 2 is V11() real ext-real Element of REAL

P + P is V11() real ext-real Element of REAL

w1 + w1 is V11() real ext-real Element of REAL

(P + P) / 2 is V11() real ext-real Element of REAL

(w1 + w1) / 2 is V11() real ext-real Element of REAL

|[((p + P) / 2),((y0 + w1) / 2)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

|[((p + P) / 2),((y0 + w1) / 2)]| `1 is V11() real ext-real Element of REAL

|[((p + P) / 2),((y0 + w1) / 2)]| `2 is V11() real ext-real Element of REAL

x1 /\ x2 is Element of K6( the carrier of (TOP-REAL 2))

Q is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))

QQ is Element of K6( the carrier of ((TOP-REAL 2) | (w2 `)))

{ |[b

{ |[b

{ |[b

{ |[b

{ |[b

r is Element of K6( the carrier of (TOP-REAL 2))

r is Element of K6( the carrier of (TOP-REAL 2))

r \/ r is Element of K6( the carrier of (TOP-REAL 2))

pa is Element of K6( the carrier of (TOP-REAL 2))

(r \/ r) \/ pa is Element of K6( the carrier of (TOP-REAL 2))

qa is Element of K6( the carrier of (TOP-REAL 2))

((r \/ r) \/ pa) \/ qa is Element of K6( the carrier of (TOP-REAL 2))

w1 + 1 is V11() real ext-real Element of REAL

P + 1 is V11() real ext-real Element of REAL

|[(P + 1),(w1 + 1)]| is V43(2) V112() V155() Element of the carrier of (TOP-REAL 2)

qa is Element of K6( the carrier of ((TOP-REAL 2) | (w2