:: JORDAN17 semantic presentation

REAL is V162() V163() V164() V168() set

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

K6(REAL) is set

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

K6(omega) is set

I[01] is TopStruct

the carrier of I[01] is set

1 is V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() 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 V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() Element of NAT

K7(2,2) is set

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

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

K246() is V96() L7()

K256() is TopSpace-like TopStruct

K6(NAT) is set

COMPLEX is V162() V168() set

RAT is V162() V163() V164() V165() V168() set

INT is V162() V163() V164() V165() V166() V168() set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() L15()

the carrier of (TOP-REAL 2) is 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

K258() is SubSpace of K256()

the carrier of K258() is set

0 is natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() Element of NAT

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

C is natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() Element of NAT

TOP-REAL C is non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() L15()

the carrier of (TOP-REAL C) is set

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

a is V43(C) V111() V154() Element of the carrier of (TOP-REAL C)

b is V43(C) V111() V154() Element of the carrier of (TOP-REAL C)

c is V43(C) V111() V154() Element of the carrier of (TOP-REAL C)

d is Element of K6( the carrier of (TOP-REAL C))

(TOP-REAL C) | d is strict SubSpace of TOP-REAL C

the carrier of ((TOP-REAL C) | d) is set

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

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

e is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL C) | d) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL C) | d)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL C) | d)))

e . 0 is set

e . 1 is set

rng e is set

[#] ((TOP-REAL C) | d) is Element of K6( the carrier of ((TOP-REAL C) | d))

K6( the carrier of ((TOP-REAL C) | d)) is set

dom e is set

c

e . c

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

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

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

e . ra is set

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

E-max C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

Lower_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

E-max C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Lower_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Lower_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (Lower_Arc C) is strict SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | (Lower_Arc C)) is set

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

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

b is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (Lower_Arc C)) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Lower_Arc C))) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Lower_Arc C))))

b . 0 is set

b . 1 is set

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

b . c is set

Lower_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

E-max C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Lower_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (Upper_Arc C) is strict SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | (Upper_Arc C)) is set

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

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

b is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (Upper_Arc C)) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Upper_Arc C))) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Upper_Arc C))))

b . 0 is set

b . 1 is set

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

b . c is set

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Lower_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

E-max C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

E-max C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (Upper_Arc C) is strict SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | (Upper_Arc C)) is set

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

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

b is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (Upper_Arc C)) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Upper_Arc C))) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Upper_Arc C))))

b . 0 is set

b . 1 is set

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

b . c is set

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

E-max C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

(TOP-REAL 2) | d is strict SubSpace of TOP-REAL 2

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

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

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

e is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | d) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | d)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | d)))

e . 0 is set

e . 1 is set

c

e . c

rng e is set

[#] ((TOP-REAL 2) | d) is Element of K6( the carrier of ((TOP-REAL 2) | d))

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

dom e is set

ra is set

e . ra is set

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

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

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

re is V11() real ext-real set

e . re is set

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

E-max C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Lower_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

(Upper_Arc C) \/ (Lower_Arc C) is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (Lower_Arc C) is strict SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | (Lower_Arc C)) is set

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

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

b is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (Lower_Arc C)) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Lower_Arc C))) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Lower_Arc C))))

b . 0 is set

b . 1 is set

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

b . c is set

d is V11() real ext-real set

dom b is set

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

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

rng b is set

[#] ((TOP-REAL 2) | (Lower_Arc C)) is Element of K6( the carrier of ((TOP-REAL 2) | (Lower_Arc C)))

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

b . d is set

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

E-max C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

Lower_Arc C is V1() Element of K6( the carrier of (TOP-REAL 2))

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

W-min C is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

e is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

C is V1() V75( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

a is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

b is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

c is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

d is V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)