:: JGRAPH_7 semantic presentation

REAL is V160() V161() V162() V166() set

NAT is V160() V161() V162() V163() V164() V165() V166() Element of K6(REAL)

K6(REAL) is set

omega is V160() V161() V162() V163() V164() V165() V166() set

K6(omega) is set

K217() is non empty strict TopSpace-like TopStruct

the carrier of K217() is non empty set

1 is non empty natural V11() real ext-real positive V112() V113() V160() V161() V162() V163() V164() V165() Element of NAT

K7(1,1) is set

K6(K7(1,1)) is set

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

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

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

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

K7(REAL,REAL) is set

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

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

2 is non empty natural V11() real ext-real positive V112() V113() V160() V161() V162() V163() V164() V165() Element of NAT

K7(2,2) is set

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

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

K245() is V94() L7()

K255() is TopSpace-like TopStruct

K6(NAT) is set

COMPLEX is V160() V166() set

RAT is V160() V161() V162() V163() V166() set

INT is V160() V161() V162() V163() V164() V166() set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like V126() V172() V173() V174() V175() V176() V177() V178() strict RLTopStruct

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

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

K7( the carrier of (TOP-REAL 2),REAL) is set

K6(K7( the carrier of (TOP-REAL 2),REAL)) is set

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

[#] (TOP-REAL 2) is non empty non proper Element of K6( the carrier of (TOP-REAL 2))

K136((TOP-REAL 2)) is V43(2) V52( TOP-REAL 2) V109() V152() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

{K136((TOP-REAL 2))} is non empty set

([#] (TOP-REAL 2)) \ {K136((TOP-REAL 2))} is Element of K6( the carrier of (TOP-REAL 2))

K7((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))) is set

K6(K7((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)))) is set

K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set

K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2))) is set

K7(COMPLEX,COMPLEX) is set

K6(K7(COMPLEX,COMPLEX)) is set

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

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

K7(RAT,RAT) is set

K6(K7(RAT,RAT)) is set

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

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

K7(INT,INT) is set

K6(K7(INT,INT)) is set

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

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

K7(NAT,NAT) is set

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

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

{} is empty V160() V161() V162() V163() V164() V165() V166() set

0 is empty natural V11() real ext-real V112() V113() V160() V161() V162() V163() V164() V165() V166() Element of NAT

K62(0,1) is V160() V161() V162() Element of K6(REAL)

I[01] is non empty strict TopSpace-like SubSpace of K255()

the carrier of I[01] is non empty set

- 1 is V11() real ext-real set

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

rectangle ((- 1),1,(- 1),1) is Element of K6( the carrier of (TOP-REAL 2))

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

K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2))) is set

closed_inside_of_rectangle ((- 1),1,(- 1),1) is Element of K6( the carrier of (TOP-REAL 2))

p2 is V11() real ext-real set

p1 is V11() real ext-real set

p3 is V11() real ext-real set

|[p1,p3]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[p2,p3]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p1,p3]|,|[p2,p3]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p2 - p1 is V11() real ext-real set

((p4 `1) - p1) / (p2 - p1) is V11() real ext-real Element of REAL

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

(p2 - p1) / (p2 - p1) is V11() real ext-real set

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

(1 - a) * |[p1,p3]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

a * |[p2,p3]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

((1 - a) * |[p1,p3]|) + (a * |[p2,p3]|) is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

(1 - a) * p1 is V11() real ext-real Element of REAL

(1 - a) * p3 is V11() real ext-real Element of REAL

|[((1 - a) * p1),((1 - a) * p3)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[((1 - a) * p1),((1 - a) * p3)]| + (a * |[p2,p3]|) is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

a * p2 is V11() real ext-real Element of REAL

a * p3 is V11() real ext-real Element of REAL

|[(a * p2),(a * p3)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[((1 - a) * p1),((1 - a) * p3)]| + |[(a * p2),(a * p3)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

((1 - a) * p1) + (a * p2) is V11() real ext-real Element of REAL

((1 - a) * p3) + (a * p3) is V11() real ext-real Element of REAL

|[(((1 - a) * p1) + (a * p2)),(((1 - a) * p3) + (a * p3))]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

a * (p2 - p1) is V11() real ext-real Element of REAL

p1 + (a * (p2 - p1)) is V11() real ext-real Element of REAL

|[(p1 + (a * (p2 - p1))),p3]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

p1 + ((p4 `1) - p1) is V11() real ext-real Element of REAL

|[(p1 + ((p4 `1) - p1)),p3]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

p1 is natural V11() real ext-real V112() V113() V160() V161() V162() V163() V164() V165() Element of NAT

TOP-REAL p1 is non empty TopSpace-like V126() V172() V173() V174() V175() V176() V177() V178() strict RLTopStruct

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

K6( the carrier of (TOP-REAL p1)) is set

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

K6(K7( the carrier of I[01], the carrier of (TOP-REAL p1))) is set

p2 is Element of K6( the carrier of (TOP-REAL p1))

p3 is V43(p1) V109() V152() Element of the carrier of (TOP-REAL p1)

p4 is V43(p1) V109() V152() Element of the carrier of (TOP-REAL p1)

(TOP-REAL p1) | p2 is strict SubSpace of TOP-REAL p1

the carrier of ((TOP-REAL p1) | p2) is set

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

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL p1) | p2))) is set

a is V19() V22( the carrier of I[01]) V23( the carrier of ((TOP-REAL p1) | p2)) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL p1) | p2)))

a . 0 is set

a . 1 is set

b is non empty V19() V22( the carrier of I[01]) V23( the carrier of (TOP-REAL p1)) Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL p1)))

rng b is Element of K6( the carrier of (TOP-REAL p1))

[#] ((TOP-REAL p1) | p2) is non proper Element of K6( the carrier of ((TOP-REAL p1) | p2))

K6( the carrier of ((TOP-REAL p1) | p2)) is set

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p3 is V11() real ext-real set

p4 is V11() real ext-real set

a is V11() real ext-real set

rectangle ((p1 `1),p3,p4,a) is Element of K6( the carrier of (TOP-REAL 2))

|[(p1 `1),p4]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[(p1 `1),a]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[(p1 `1),p4]|,|[(p1 `1),a]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p3 is V11() real ext-real set

p4 is V11() real ext-real set

rectangle ((p1 `1),p3,p4,(p2 `2)) is Element of K6( the carrier of (TOP-REAL 2))

|[(p1 `1),p4]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[(p1 `1),(p2 `2)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[(p1 `1),p4]|,|[(p1 `1),(p2 `2)]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

|[p3,(p2 `2)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[(p1 `1),(p2 `2)]|,|[p3,(p2 `2)]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p4 is V11() real ext-real set

p3 is V11() real ext-real set

rectangle ((p1 `1),(p2 `1),p3,p4) is Element of K6( the carrier of (TOP-REAL 2))

|[(p2 `1),p3]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[(p2 `1),p4]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[(p2 `1),p3]|,|[(p2 `1),p4]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

|[(p1 `1),p3]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[(p1 `1),p4]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[(p1 `1),p3]|,|[(p1 `1),p4]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p4 is V11() real ext-real set

p3 is V11() real ext-real set

rectangle ((p1 `1),p3,(p2 `2),p4) is Element of K6( the carrier of (TOP-REAL 2))

|[(p1 `1),(p2 `2)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[(p1 `1),p4]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[(p1 `1),(p2 `2)]|,|[(p1 `1),p4]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

W-min (rectangle ((p1 `1),p3,(p2 `2),p4)) is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

(W-min (rectangle ((p1 `1),p3,(p2 `2),p4))) `1 is V11() real ext-real Element of REAL

|[p3,(p2 `2)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p3,(p2 `2)]|,|[(p1 `1),(p2 `2)]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p4 is V11() real ext-real set

p3 is V11() real ext-real set

b is V11() real ext-real set

a is V11() real ext-real set

rectangle (p3,p4,a,b) is Element of K6( the carrier of (TOP-REAL 2))

|[p3,b]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[p4,b]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p3,b]|,|[p4,b]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p4 is V11() real ext-real set

p3 is V11() real ext-real set

b is V11() real ext-real set

a is V11() real ext-real set

rectangle (p3,p4,a,b) is Element of K6( the carrier of (TOP-REAL 2))

|[p4,b]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[p4,a]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p4,b]|,|[p4,a]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

|[p3,b]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p3,b]|,|[p4,b]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p4 is V11() real ext-real set

p3 is V11() real ext-real set

b is V11() real ext-real set

a is V11() real ext-real set

rectangle (p3,p4,a,b) is Element of K6( the carrier of (TOP-REAL 2))

|[p4,a]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[p3,a]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p4,a]|,|[p3,a]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

W-min (rectangle (p3,p4,a,b)) is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

(W-min (rectangle (p3,p4,a,b))) `1 is V11() real ext-real Element of REAL

|[p3,b]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[p4,b]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p3,b]|,|[p4,b]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p4 is V11() real ext-real set

p3 is V11() real ext-real set

b is V11() real ext-real set

a is V11() real ext-real set

rectangle (p3,p4,a,b) is Element of K6( the carrier of (TOP-REAL 2))

|[p4,b]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[p4,a]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p4,b]|,|[p4,a]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p4 is V11() real ext-real set

p3 is V11() real ext-real set

b is V11() real ext-real set

a is V11() real ext-real set

rectangle (p3,p4,a,b) is Element of K6( the carrier of (TOP-REAL 2))

|[p4,b]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[p4,a]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p4,b]|,|[p4,a]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

W-min (rectangle (p3,p4,a,b)) is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[p3,a]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

(W-min (rectangle (p3,p4,a,b))) `1 is V11() real ext-real Element of REAL

LSeg (|[p4,a]|,|[p3,a]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p4 is V11() real ext-real set

p3 is V11() real ext-real set

b is V11() real ext-real set

a is V11() real ext-real set

rectangle (p3,p4,a,b) is Element of K6( the carrier of (TOP-REAL 2))

|[p4,a]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[p3,a]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p4,a]|,|[p3,a]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

W-min (rectangle (p3,p4,a,b)) is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

(W-min (rectangle (p3,p4,a,b))) `1 is V11() real ext-real Element of REAL

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

p4 is V11() real ext-real set

p3 is V11() real ext-real set

b is V11() real ext-real set

a is V11() real ext-real set

rectangle (p3,p4,a,b) is Element of K6( the carrier of (TOP-REAL 2))

|[p4,b]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[p4,a]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p4,b]|,|[p4,a]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

|[p3,b]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

LSeg (|[p3,b]|,|[p4,b]|) is Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

c is V11() real ext-real set

d is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p2 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p3 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p4 is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

b is V11() real ext-real set

a is V11() real ext-real set

d is V11() real ext-real set

c is V11() real ext-real set

rectangle (a,b,c,d) is Element of K6( the carrier of (TOP-REAL 2))

p1 is V11() real ext-real set

p3 is V11() real ext-real set

p2 is V11() real ext-real set

p4 is V11() real ext-real set

AffineMap (p1,p2,p3,p4) is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total continuous Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

1 / p1 is V11() real ext-real Element of REAL

p2 / p1 is V11() real ext-real set

- (p2 / p1) is V11() real ext-real set

1 / p3 is V11() real ext-real Element of REAL

p4 / p3 is V11() real ext-real set

- (p4 / p3) is V11() real ext-real set

AffineMap ((1 / p1),(- (p2 / p1)),(1 / p3),(- (p4 / p3))) is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total continuous Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

a is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

b is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

a " is V19() Function-like set

b " is V19() Function-like set

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

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

c is set

d is set

a . c is set

b . d is set

Q is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

a . Q is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p1 * (Q `1) is V11() real ext-real Element of REAL

(p1 * (Q `1)) + p2 is V11() real ext-real Element of REAL

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

p3 * (Q `2) is V11() real ext-real Element of REAL

(p3 * (Q `2)) + p4 is V11() real ext-real Element of REAL

|[((p1 * (Q `1)) + p2),((p3 * (Q `2)) + p4)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

P is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

((1 / p1) * (P `1)) + (- (p2 / p1)) is V11() real ext-real Element of REAL

(1 / p1) * p1 is V11() real ext-real Element of REAL

((1 / p1) * p1) * (Q `1) is V11() real ext-real Element of REAL

(1 / p1) * p2 is V11() real ext-real Element of REAL

(((1 / p1) * p1) * (Q `1)) + ((1 / p1) * p2) is V11() real ext-real Element of REAL

((((1 / p1) * p1) * (Q `1)) + ((1 / p1) * p2)) + (- (p2 / p1)) is V11() real ext-real Element of REAL

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

(1 * (Q `1)) + ((1 / p1) * p2) is V11() real ext-real Element of REAL

((1 * (Q `1)) + ((1 / p1) * p2)) + (- (p2 / p1)) is V11() real ext-real Element of REAL

(Q `1) + (p2 / p1) is V11() real ext-real Element of REAL

((Q `1) + (p2 / p1)) + (- (p2 / p1)) is V11() real ext-real Element of REAL

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

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

((1 / p3) * (P `2)) + (- (p4 / p3)) is V11() real ext-real Element of REAL

(1 / p3) * p3 is V11() real ext-real Element of REAL

((1 / p3) * p3) * (Q `2) is V11() real ext-real Element of REAL

(1 / p3) * p4 is V11() real ext-real Element of REAL

(((1 / p3) * p3) * (Q `2)) + ((1 / p3) * p4) is V11() real ext-real Element of REAL

((((1 / p3) * p3) * (Q `2)) + ((1 / p3) * p4)) + (- (p4 / p3)) is V11() real ext-real Element of REAL

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

(1 * (Q `2)) + ((1 / p3) * p4) is V11() real ext-real Element of REAL

((1 * (Q `2)) + ((1 / p3) * p4)) + (- (p4 / p3)) is V11() real ext-real Element of REAL

(Q `2) + (p4 / p3) is V11() real ext-real Element of REAL

((Q `2) + (p4 / p3)) + (- (p4 / p3)) is V11() real ext-real Element of REAL

b . P is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[(((1 / p1) * (P `1)) + (- (p2 / p1))),(((1 / p3) * (P `2)) + (- (p4 / p3)))]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

P is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

b . P is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

((1 / p1) * (P `1)) + (- (p2 / p1)) is V11() real ext-real Element of REAL

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

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

((1 / p3) * (P `2)) + (- (p4 / p3)) is V11() real ext-real Element of REAL

|[(((1 / p1) * (P `1)) + (- (p2 / p1))),(((1 / p3) * (P `2)) + (- (p4 / p3)))]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

Q is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

p1 * (Q `1) is V11() real ext-real Element of REAL

(p1 * (Q `1)) + p2 is V11() real ext-real Element of REAL

p1 * (1 / p1) is V11() real ext-real Element of REAL

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

p1 * (- (p2 / p1)) is V11() real ext-real set

((p1 * (1 / p1)) * (P `1)) + (p1 * (- (p2 / p1))) is V11() real ext-real Element of REAL

(((p1 * (1 / p1)) * (P `1)) + (p1 * (- (p2 / p1)))) + p2 is V11() real ext-real Element of REAL

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

(1 * (P `1)) + (p1 * (- (p2 / p1))) is V11() real ext-real Element of REAL

((1 * (P `1)) + (p1 * (- (p2 / p1)))) + p2 is V11() real ext-real Element of REAL

- p2 is V11() real ext-real set

(- p2) / p1 is V11() real ext-real set

p1 * ((- p2) / p1) is V11() real ext-real set

(P `1) + (p1 * ((- p2) / p1)) is V11() real ext-real Element of REAL

((P `1) + (p1 * ((- p2) / p1))) + p2 is V11() real ext-real Element of REAL

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

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

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

p3 * (Q `2) is V11() real ext-real Element of REAL

(p3 * (Q `2)) + p4 is V11() real ext-real Element of REAL

p3 * (1 / p3) is V11() real ext-real Element of REAL

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

p3 * (- (p4 / p3)) is V11() real ext-real set

((p3 * (1 / p3)) * (P `2)) + (p3 * (- (p4 / p3))) is V11() real ext-real Element of REAL

(((p3 * (1 / p3)) * (P `2)) + (p3 * (- (p4 / p3)))) + p4 is V11() real ext-real Element of REAL

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

(1 * (P `2)) + (p3 * (- (p4 / p3))) is V11() real ext-real Element of REAL

((1 * (P `2)) + (p3 * (- (p4 / p3)))) + p4 is V11() real ext-real Element of REAL

- p4 is V11() real ext-real set

(- p4) / p3 is V11() real ext-real set

p3 * ((- p4) / p3) is V11() real ext-real set

(P `2) + (p3 * ((- p4) / p3)) is V11() real ext-real Element of REAL

((P `2) + (p3 * ((- p4) / p3))) + p4 is V11() real ext-real Element of REAL

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

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

a . Q is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

|[((p1 * (Q `1)) + p2),((p3 * (Q `2)) + p4)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

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

1 / d is V11() real ext-real Element of REAL

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

c / d is V11() real ext-real Element of REAL

- (c / d) is V11() real ext-real Element of REAL

AffineMap ((1 / Q),(- (P / Q)),(1 / d),(- (c / d))) is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total continuous Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

AffineMap (Q,P,d,c) is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total continuous Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

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

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

p1 is V11() real ext-real set

p3 is V11() real ext-real set

p2 is V11() real ext-real set

p4 is V11() real ext-real set

AffineMap (p1,p2,p3,p4) is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total continuous Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

a is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

1 / p1 is V11() real ext-real Element of REAL

p2 / p1 is V11() real ext-real set

- (p2 / p1) is V11() real ext-real set

1 / p3 is V11() real ext-real Element of REAL

p4 / p3 is V11() real ext-real set

- (p4 / p3) is V11() real ext-real set

AffineMap ((1 / p1),(- (p2 / p1)),(1 / p3),(- (p4 / p3))) is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total continuous Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

a " is V19() Function-like set

d is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

c is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

a . d is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

(a . d) `1 is V11() real ext-real Element of REAL

a . c is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

(a . c) `1 is V11() real ext-real Element of REAL

p1 * (c `1) is V11() real ext-real Element of REAL

(p1 * (c `1)) + p2 is V11() real ext-real Element of REAL

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

p3 * (c `2) is V11() real ext-real Element of REAL

(p3 * (c `2)) + p4 is V11() real ext-real Element of REAL

|[((p1 * (c `1)) + p2),((p3 * (c `2)) + p4)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

p1 * (d `1) is V11() real ext-real Element of REAL

(p1 * (d `1)) + p2 is V11() real ext-real Element of REAL

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

p3 * (d `2) is V11() real ext-real Element of REAL

(p3 * (d `2)) + p4 is V11() real ext-real Element of REAL

|[((p1 * (d `1)) + p2),((p3 * (d `2)) + p4)]| is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

dom (AffineMap ((1 / p1),(- (p2 / p1)),(1 / p3),(- (p4 / p3)))) is Element of K6( the carrier of (TOP-REAL 2))

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

a /" is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

d is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

c is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

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

a . d is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

(a . d) `1 is V11() real ext-real Element of REAL

a . c is V43(2) V109() V152() Element of the carrier of (TOP-REAL 2)

(a . c) `1 is V11() real ext-real Element of REAL

p1 is V11() real ext-real set

p3 is V11() real ext-real set

p2 is V11() real ext-real set

p4 is V11() real ext-real set

AffineMap (p1,p2,p3,p4) is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total continuous Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

a is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( the carrier of (TOP-REAL 2)) Function-like V29( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

1 / p1 is V11() real ext-real Element of REAL

p2 / p1 is V11() real ext-real set

- (p2 / p1) is V11() real ext-real set

1 / p3 is V11() real ext-real Element of REAL

p4 / p3 is V11() real ext-real set

- (p4 / p3) is V11() real ext-real set

AffineMap (