environ
vocabularies HIDDEN, TOPREAL2, SUBSET_1, EUCLID, PRE_TOPC, NUMBERS, RELAT_1, STRUCT_0, FUNCT_1, XBOOLE_0, JORDAN2C, XXREAL_2, REAL_1, ARYTM_3, CONVEX1, MCART_1, RLTOPSP1, ARYTM_1, CARD_1, XXREAL_0, TOPREAL1, TARSKI, JORDAN6, PSCOMP_1, RCOMP_1, RELAT_2, SPPOL_1, JORDAN3, JORDAN21, SEQ_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, XXREAL_0, XCMPLX_0, REAL_1, FUNCT_1, RELSET_1, SEQ_4, DOMAIN_1, XXREAL_2, STRUCT_0, PRE_TOPC, COMPTS_1, CONNSP_1, TBSP_1, RCOMP_1, PSCOMP_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, JORDAN2C, SPPOL_1, JORDAN6, JORDAN5C;
definitions TARSKI, XBOOLE_0, JORDAN1;
theorems XBOOLE_1, JORDAN6, XBOOLE_0, EUCLID, TOPREAL1, BORSUK_4, TARSKI, TOPREAL5, JORDAN16, JORDAN7, JGRAPH_1, TBSP_1, JORDAN2C, PSCOMP_1, SPRECT_1, JORDAN5B, SPPOL_1, TOPREAL3, SEQ_4, FUNCT_2, RELAT_1, TOPS_1, RCOMP_1, JCT_MISC, XREAL_1, TOPREAL6, XXREAL_0, XXREAL_2, RLTOPSP1;
schemes ;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2, TOPREAL5, JORDAN6, TOPREAL6, RLTOPSP1, JORDAN2C;
constructors HIDDEN, REAL_1, RCOMP_1, CONNSP_1, COMPTS_1, TBSP_1, TOPREAL1, SPPOL_1, PSCOMP_1, JORDAN5C, JORDAN6, JORDAN2C, SEQ_4, CONVEX1, BINOP_2, TOPMETR, COMPLEX1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities RLTOPSP1, PSCOMP_1, SUBSET_1;
expansions TARSKI, XBOOLE_0;
Lm1:
dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
Lm2:
for r being Real
for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
Lm3:
now for a, A, B, C being set holds
( not a in (A \/ B) \/ C or a in A or a in B or a in C )
end;
Lm4:
for A, B, C, D being set st A misses D & B misses D & C misses D holds
(A \/ B) \/ C misses D
theorem Th11:
for
P being
Subset of the
carrier of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
p1 <> q1 &
p2 <> q2 holds
( not
p1 in Segment (
P,
p1,
p2,
q1,
q2) & not
p2 in Segment (
P,
p1,
p2,
q1,
q2) )