environ
vocabularies HIDDEN, NUMBERS, TOPREAL2, PRE_TOPC, EUCLID, SUBSET_1, TOPREAL1, FUNCT_1, BORSUK_1, RELAT_1, REAL_1, TOPS_2, CARD_1, XXREAL_0, STRUCT_0, XXREAL_1, JORDAN3, PSCOMP_1, JORDAN6, ARYTM_3, XBOOLE_0, JORDAN17;
notations HIDDEN, ORDINAL1, SUBSET_1, NUMBERS, XREAL_0, REAL_1, RCOMP_1, STRUCT_0, RELAT_1, FUNCT_1, TOPREAL1, TOPREAL2, PRE_TOPC, TOPS_2, BORSUK_1, EUCLID, JORDAN5C, PSCOMP_1, JORDAN6, XXREAL_0;
definitions TOPREAL1;
theorems XBOOLE_0, JORDAN5C, JORDAN6, JORDAN7, TOPS_2, FUNCT_1, BORSUK_1, PRE_TOPC, TOPREAL5, SPRECT_1, JORDAN16, XREAL_1, XXREAL_0, XXREAL_1;
schemes ;
registrations RELSET_1, XREAL_0, MEMBERED, TOPREAL2, EUCLID;
constructors HIDDEN, REAL_1, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, PSCOMP_1, JORDAN5C, JORDAN6, COMPLEX1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE;
equalities STRUCT_0;
expansions ;
theorem Th6:
for
a,
b,
c,
d being
Point of
(TOP-REAL 2) for
P being
Subset of
(TOP-REAL 2) st
a <> b &
P is_an_arc_of c,
d &
LE a,
b,
P,
c,
d holds
ex
e being
Point of
(TOP-REAL 2) st
(
a <> e &
b <> e &
LE a,
e,
P,
c,
d &
LE e,
b,
P,
c,
d )
definition
let P be
Subset of
(TOP-REAL 2);
let a,
b,
c,
d be
Point of
(TOP-REAL 2);
pred a,
b,
c,
d are_in_this_order_on P means
( (
LE a,
b,
P &
LE b,
c,
P &
LE c,
d,
P ) or (
LE b,
c,
P &
LE c,
d,
P &
LE d,
a,
P ) or (
LE c,
d,
P &
LE d,
a,
P &
LE a,
b,
P ) or (
LE d,
a,
P &
LE a,
b,
P &
LE b,
c,
P ) );
end;
::
deftheorem defines
are_in_this_order_on JORDAN17:def 1 :
for P being Subset of (TOP-REAL 2)
for a, b, c, d being Point of (TOP-REAL 2) holds
( a,b,c,d are_in_this_order_on P iff ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) );
theorem
for
C being
Simple_closed_curve for
a,
b,
c,
d being
Point of
(TOP-REAL 2) st
a in C &
b in C &
c in C &
d in C & not
a,
b,
c,
d are_in_this_order_on C & not
a,
b,
d,
c are_in_this_order_on C & not
a,
c,
b,
d are_in_this_order_on C & not
a,
c,
d,
b are_in_this_order_on C & not
a,
d,
b,
c are_in_this_order_on C holds
a,
d,
c,
b are_in_this_order_on C