:: 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
c7 is set
e . c7 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
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
c7 is V11() real ext-real Element of REAL
e . c7 is set
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)