environ
vocabularies HIDDEN, NUMBERS, TOPREAL2, SUBSET_1, EUCLID, PRE_TOPC, TARSKI, XBOOLE_0, JORDAN6, PSCOMP_1, TOPREAL1, JORDAN3, FUNCT_1, ORDINAL2, CONNSP_2, RCOMP_1, RELAT_1, TOPS_2, FUNCT_2, STRUCT_0, BORSUK_1, CARD_1, REAL_1, ARYTM_3, XXREAL_0, XXREAL_1, PCOMPS_1, JGRAPH_2, ARYTM_1, TOPMETR;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FCONT_1, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, CONNSP_2, PCOMPS_1, RCOMP_1, TMAP_1, EUCLID, PSCOMP_1, TOPMETR, JORDAN6, TOPREAL1, JORDAN5C, TOPREAL2, JORDAN7;
definitions TARSKI, TOPS_2, TOPREAL1, BORSUK_1;
theorems PRE_TOPC, TOPMETR, XBOOLE_0, FUNCT_1, XBOOLE_1, FUNCT_2, TOPREAL5, TREAL_1, BORSUK_1, JORDAN6, TOPREAL1, TOPS_2, TARSKI, RELAT_1, TOPREAL3, JORDAN5B, TOPMETR3, TOPREAL2, ZFMISC_1, JORDAN5A, JORDAN5C, FCONT_1, FUNCT_3, CONNSP_2, TMAP_1, RFUNCT_2, RELSET_1, FUNCT_4, JORDAN7, SPRECT_1, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1, EUCLID, XREAL_0;
schemes ;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID, TOPMETR, TOPREAL2, TMAP_1, ORDINAL1;
constructors HIDDEN, REAL_1, RCOMP_1, FCONT_1, TOPS_2, TMAP_1, TOPMETR, PCOMPS_1, TOPREAL1, PSCOMP_1, JORDAN5C, JORDAN6, JORDAN7, COMPLEX1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0;
expansions TARSKI, TOPS_2, TOPREAL1, BORSUK_1;
theorem Th5:
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
LE q1,
q2,
A,
p1,
p2 holds
(
q1 in Segment (
A,
p1,
p2,
q1,
q2) &
q2 in Segment (
A,
p1,
p2,
q1,
q2) )
theorem Th16:
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 holds
ex
g being
Function of
I[01],
((TOP-REAL 2) | A) ex
s1,
s2 being
Real st
(
g is
being_homeomorphism &
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 &
g . s2 = q2 &
0 <= s1 &
s1 <= s2 &
s2 <= 1 )
theorem Th17:
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 &
q1 <> q2 holds
ex
g being
Function of
I[01],
((TOP-REAL 2) | A) ex
s1,
s2 being
Real st
(
g is
being_homeomorphism &
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 &
g . s2 = q2 &
0 <= s1 &
s1 < s2 &
s2 <= 1 )
theorem
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
LE q1,
q2,
A,
p1,
p2 holds
not
Segment (
A,
p1,
p2,
q1,
q2) is
empty
theorem Th21:
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 &
q1 <> q2 holds
Segment (
A,
p1,
p2,
q1,
q2)
is_an_arc_of q1,
q2