environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, EUCLID, PRE_TOPC, TOPREAL1, JORDAN6, JORDAN3, TARSKI, REAL_1, RLTOPSP1, MCART_1, XXREAL_0, ARYTM_1, RELAT_1, ARYTM_3, CARD_1, SUPINF_2, SPPOL_2, FINSEQ_1, PARTFUN1, XBOOLE_0, FUNCT_1, TOPMETR, BORSUK_1, TOPS_2, ORDINAL2, XXREAL_1, SEQ_4, STRUCT_0, XXREAL_2, METRIC_1, COMPLEX1, RCOMP_1, PCOMPS_1, RELAT_2, BORSUK_2, GRAPH_1, TOPREAL4, NAT_1, JORDAN20, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, NAT_D, PARTFUN1, FUNCT_2, SEQ_4, FINSEQ_1, STRUCT_0, CONNSP_1, RCOMP_1, METRIC_1, PCOMPS_1, JORDAN5C, JORDAN6, RLVECT_1, RLTOPSP1, EUCLID, TOPMETR, PRE_TOPC, TOPS_2, NUMBERS, PSCOMP_1, BORSUK_2, TOPREAL4, TOPREAL1, SPPOL_2, FINSEQ_6;
definitions TARSKI;
theorems TARSKI, TOPREAL1, XBOOLE_0, JORDAN6, TOPS_2, XBOOLE_1, SEQ_4, RELAT_1, PSCOMP_1, FUNCT_2, TOPREAL3, JORDAN5C, TOPREAL5, RCOMP_1, TOPMETR, ABSVALUE, METRIC_1, JORDAN16, XREAL_0, FUNCT_1, PRE_TOPC, BORSUK_1, BORSUK_4, FRECHET, PCOMPS_1, NAT_1, XCMPLX_1, JORDAN2B, UNIFORM1, GOBOARD6, TREAL_1, BORSUK_2, CONNSP_1, TOPMETR3, JORDAN5B, GOBOARD7, JGRAPH_2, TOPREAL4, FINSEQ_4, FINSEQ_1, SPRECT_4, SPRECT_3, FINSEQ_3, XREAL_1, COMPLEX1, XXREAL_0, PARTFUN1, XXREAL_1, XXREAL_2, NAT_D, RLTOPSP1, FINSEQ_6, RLVECT_1;
schemes NAT_1;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, TOPMETR, XXREAL_2, RLTOPSP1, RELAT_1, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, RCOMP_1, CONNSP_1, TOPS_2, TOPREAL1, TOPREAL4, PSCOMP_1, BORSUK_2, JORDAN5C, JORDAN6, BINOP_2, NAT_D, SEQ_4, CONVEX1, FINSEQ_6, PCOMPS_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, RLTOPSP1;
expansions TARSKI;
definition
let P be
Subset of
(TOP-REAL 2);
let p1,
p2,
p be
Point of
(TOP-REAL 2);
let e be
Real;
pred p is_Lin P,
p1,
p2,
e means
(
P is_an_arc_of p1,
p2 &
p in P &
p `1 = e & ex
p4 being
Point of
(TOP-REAL 2) st
(
p4 `1 < e &
LE p4,
p,
P,
p1,
p2 & ( for
p5 being
Point of
(TOP-REAL 2) st
LE p4,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 holds
p5 `1 <= e ) ) );
pred p is_Rin P,
p1,
p2,
e means
(
P is_an_arc_of p1,
p2 &
p in P &
p `1 = e & ex
p4 being
Point of
(TOP-REAL 2) st
(
p4 `1 > e &
LE p4,
p,
P,
p1,
p2 & ( for
p5 being
Point of
(TOP-REAL 2) st
LE p4,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 holds
p5 `1 >= e ) ) );
pred p is_Lout P,
p1,
p2,
e means
(
P is_an_arc_of p1,
p2 &
p in P &
p `1 = e & ex
p4 being
Point of
(TOP-REAL 2) st
(
p4 `1 < e &
LE p,
p4,
P,
p1,
p2 & ( for
p5 being
Point of
(TOP-REAL 2) st
LE p5,
p4,
P,
p1,
p2 &
LE p,
p5,
P,
p1,
p2 holds
p5 `1 <= e ) ) );
pred p is_Rout P,
p1,
p2,
e means
(
P is_an_arc_of p1,
p2 &
p in P &
p `1 = e & ex
p4 being
Point of
(TOP-REAL 2) st
(
p4 `1 > e &
LE p,
p4,
P,
p1,
p2 & ( for
p5 being
Point of
(TOP-REAL 2) st
LE p5,
p4,
P,
p1,
p2 &
LE p,
p5,
P,
p1,
p2 holds
p5 `1 >= e ) ) );
pred p is_OSin P,
p1,
p2,
e means
(
P is_an_arc_of p1,
p2 &
p in P &
p `1 = e & ex
p7 being
Point of
(TOP-REAL 2) st
(
LE p7,
p,
P,
p1,
p2 & ( for
p8 being
Point of
(TOP-REAL 2) st
LE p7,
p8,
P,
p1,
p2 &
LE p8,
p,
P,
p1,
p2 holds
p8 `1 = e ) & ( for
p4 being
Point of
(TOP-REAL 2) st
LE p4,
p7,
P,
p1,
p2 &
p4 <> p7 holds
( ex
p5 being
Point of
(TOP-REAL 2) st
(
LE p4,
p5,
P,
p1,
p2 &
LE p5,
p7,
P,
p1,
p2 &
p5 `1 > e ) & ex
p6 being
Point of
(TOP-REAL 2) st
(
LE p4,
p6,
P,
p1,
p2 &
LE p6,
p7,
P,
p1,
p2 &
p6 `1 < e ) ) ) ) );
pred p is_OSout P,
p1,
p2,
e means
(
P is_an_arc_of p1,
p2 &
p in P &
p `1 = e & ex
p7 being
Point of
(TOP-REAL 2) st
(
LE p,
p7,
P,
p1,
p2 & ( for
p8 being
Point of
(TOP-REAL 2) st
LE p8,
p7,
P,
p1,
p2 &
LE p,
p8,
P,
p1,
p2 holds
p8 `1 = e ) & ( for
p4 being
Point of
(TOP-REAL 2) st
LE p7,
p4,
P,
p1,
p2 &
p4 <> p7 holds
( ex
p5 being
Point of
(TOP-REAL 2) st
(
LE p5,
p4,
P,
p1,
p2 &
LE p7,
p5,
P,
p1,
p2 &
p5 `1 > e ) & ex
p6 being
Point of
(TOP-REAL 2) st
(
LE p6,
p4,
P,
p1,
p2 &
LE p7,
p6,
P,
p1,
p2 &
p6 `1 < e ) ) ) ) );
correctness
;
end;
::
deftheorem defines
is_Lin JORDAN20:def 1 :
for P being Subset of (TOP-REAL 2)
for p1, p2, p being Point of (TOP-REAL 2)
for e being Real holds
( p is_Lin P,p1,p2,e iff ( P is_an_arc_of p1,p2 & p in P & p `1 = e & ex p4 being Point of (TOP-REAL 2) st
( p4 `1 < e & LE p4,p,P,p1,p2 & ( for p5 being Point of (TOP-REAL 2) st LE p4,p5,P,p1,p2 & LE p5,p,P,p1,p2 holds
p5 `1 <= e ) ) ) );
::
deftheorem defines
is_Rin JORDAN20:def 2 :
for P being Subset of (TOP-REAL 2)
for p1, p2, p being Point of (TOP-REAL 2)
for e being Real holds
( p is_Rin P,p1,p2,e iff ( P is_an_arc_of p1,p2 & p in P & p `1 = e & ex p4 being Point of (TOP-REAL 2) st
( p4 `1 > e & LE p4,p,P,p1,p2 & ( for p5 being Point of (TOP-REAL 2) st LE p4,p5,P,p1,p2 & LE p5,p,P,p1,p2 holds
p5 `1 >= e ) ) ) );
::
deftheorem defines
is_Lout JORDAN20:def 3 :
for P being Subset of (TOP-REAL 2)
for p1, p2, p being Point of (TOP-REAL 2)
for e being Real holds
( p is_Lout P,p1,p2,e iff ( P is_an_arc_of p1,p2 & p in P & p `1 = e & ex p4 being Point of (TOP-REAL 2) st
( p4 `1 < e & LE p,p4,P,p1,p2 & ( for p5 being Point of (TOP-REAL 2) st LE p5,p4,P,p1,p2 & LE p,p5,P,p1,p2 holds
p5 `1 <= e ) ) ) );
::
deftheorem defines
is_Rout JORDAN20:def 4 :
for P being Subset of (TOP-REAL 2)
for p1, p2, p being Point of (TOP-REAL 2)
for e being Real holds
( p is_Rout P,p1,p2,e iff ( P is_an_arc_of p1,p2 & p in P & p `1 = e & ex p4 being Point of (TOP-REAL 2) st
( p4 `1 > e & LE p,p4,P,p1,p2 & ( for p5 being Point of (TOP-REAL 2) st LE p5,p4,P,p1,p2 & LE p,p5,P,p1,p2 holds
p5 `1 >= e ) ) ) );
::
deftheorem defines
is_OSin JORDAN20:def 5 :
for P being Subset of (TOP-REAL 2)
for p1, p2, p being Point of (TOP-REAL 2)
for e being Real holds
( p is_OSin P,p1,p2,e iff ( P is_an_arc_of p1,p2 & p in P & p `1 = e & ex p7 being Point of (TOP-REAL 2) st
( LE p7,p,P,p1,p2 & ( for p8 being Point of (TOP-REAL 2) st LE p7,p8,P,p1,p2 & LE p8,p,P,p1,p2 holds
p8 `1 = e ) & ( for p4 being Point of (TOP-REAL 2) st LE p4,p7,P,p1,p2 & p4 <> p7 holds
( ex p5 being Point of (TOP-REAL 2) st
( LE p4,p5,P,p1,p2 & LE p5,p7,P,p1,p2 & p5 `1 > e ) & ex p6 being Point of (TOP-REAL 2) st
( LE p4,p6,P,p1,p2 & LE p6,p7,P,p1,p2 & p6 `1 < e ) ) ) ) ) );
::
deftheorem defines
is_OSout JORDAN20:def 6 :
for P being Subset of (TOP-REAL 2)
for p1, p2, p being Point of (TOP-REAL 2)
for e being Real holds
( p is_OSout P,p1,p2,e iff ( P is_an_arc_of p1,p2 & p in P & p `1 = e & ex p7 being Point of (TOP-REAL 2) st
( LE p,p7,P,p1,p2 & ( for p8 being Point of (TOP-REAL 2) st LE p8,p7,P,p1,p2 & LE p,p8,P,p1,p2 holds
p8 `1 = e ) & ( for p4 being Point of (TOP-REAL 2) st LE p7,p4,P,p1,p2 & p4 <> p7 holds
( ex p5 being Point of (TOP-REAL 2) st
( LE p5,p4,P,p1,p2 & LE p7,p5,P,p1,p2 & p5 `1 > e ) & ex p6 being Point of (TOP-REAL 2) st
( LE p6,p4,P,p1,p2 & LE p7,p6,P,p1,p2 & p6 `1 < e ) ) ) ) ) );
theorem
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
p being
Point of
(TOP-REAL 2) for
e being
Real st
P is_an_arc_of p1,
p2 &
p1 `1 < e &
p in P &
p `1 = e & not
p is_Lin P,
p1,
p2,
e & not
p is_Rin P,
p1,
p2,
e holds
p is_OSin P,
p1,
p2,
e
theorem
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
p being
Point of
(TOP-REAL 2) for
e being
Real st
P is_an_arc_of p1,
p2 &
p2 `1 > e &
p in P &
p `1 = e & not
p is_Lout P,
p1,
p2,
e & not
p is_Rout P,
p1,
p2,
e holds
p is_OSout P,
p1,
p2,
e
Lm1:
[#] I[01] <> {}
;
theorem Th19:
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
q1 in P &
q2 in P & not
LE q1,
q2,
P,
p1,
p2 holds
LE q2,
q1,
P,
p1,
p2
theorem Th22:
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2,
q3 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
LE q1,
q2,
P,
p1,
p2 &
LE q2,
q3,
P,
p1,
p2 holds
(Segment (P,p1,p2,q1,q2)) \/ (Segment (P,p1,p2,q2,q3)) = Segment (
P,
p1,
p2,
q1,
q3)
theorem
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2,
q3 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
LE q1,
q2,
P,
p1,
p2 &
LE q2,
q3,
P,
p1,
p2 holds
(Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) = {q2}
theorem Th25:
for
P,
Q1 being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
Q1 is_an_arc_of q1,
q2 &
LE q1,
q2,
P,
p1,
p2 &
Q1 c= P holds
Q1 = Segment (
P,
p1,
p2,
q1,
q2)
theorem
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2,
p being
Point of
(TOP-REAL 2) for
e being
Real st
q1 is_Lin P,
p1,
p2,
e &
q2 `1 = e &
LSeg (
q1,
q2)
c= P &
p in LSeg (
q1,
q2) holds
p is_Lin P,
p1,
p2,
e
theorem
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2,
p being
Point of
(TOP-REAL 2) for
e being
Real st
q1 is_Rin P,
p1,
p2,
e &
q2 `1 = e &
LSeg (
q1,
q2)
c= P &
p in LSeg (
q1,
q2) holds
p is_Rin P,
p1,
p2,
e
theorem
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2,
p being
Point of
(TOP-REAL 2) for
e being
Real st
q1 is_Lout P,
p1,
p2,
e &
q2 `1 = e &
LSeg (
q1,
q2)
c= P &
p in LSeg (
q1,
q2) holds
p is_Lout P,
p1,
p2,
e
theorem
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2,
p being
Point of
(TOP-REAL 2) for
e being
Real st
q1 is_Rout P,
p1,
p2,
e &
q2 `1 = e &
LSeg (
q1,
q2)
c= P &
p in LSeg (
q1,
q2) holds
p is_Rout P,
p1,
p2,
e