environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, NAT_1, ARYTM_3, XXREAL_0, ARYTM_1, FINSEQ_1, XBOOLE_0, RELAT_1, FINSET_1, TARSKI, COMPLEX1, REAL_1, PRE_TOPC, EUCLID, METRIC_1, FUNCT_1, RCOMP_1, RLTOPSP1, CARD_1, SEQ_4, XXREAL_2, PCOMPS_1, STRUCT_0, SUPINF_2, TEX_2, COMPTS_1, TOPREAL1, BORSUK_1, TOPS_2, ORDINAL2, MCART_1, ZFMISC_1, PARTFUN1, SETFAM_1, SPPOL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XXREAL_0, XXREAL_2, XREAL_0, XCMPLX_0, COMPLEX1, REAL_1, NAT_1, SEQ_4, FUNCT_1, BINOP_1, PARTFUN1, PRE_TOPC, BORSUK_1, FINSET_1, FINSEQ_1, FINSEQ_4, DOMAIN_1, STRUCT_0, METRIC_1, PCOMPS_1, TOPS_2, ZFMISC_1, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, TEX_2, TOPREAL1;
definitions TARSKI, TOPREAL1, XXREAL_2;
theorems TARSKI, NAT_1, INT_1, ABSVALUE, SUBSET_1, FINSET_1, FINSEQ_1, PRE_TOPC, METRIC_1, TOPS_1, TOPS_2, SEQ_4, EUCLID, TOPMETR, TOPREAL1, TOPREAL3, COMPTS_1, TEX_2, FINSEQ_3, ZFMISC_1, HEINE, TDLAT_3, PARTFUN2, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, RLTOPSP1, RLVECT_1;
schemes FRAENKEL;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TEX_2, EUCLID, TOPREAL1, FINSET_1, VALUED_0, RLTOPSP1, FUNCT_1;
constructors HIDDEN, SETFAM_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, SEQ_4, FINSEQ_4, TOPS_2, COMPTS_1, REALSET2, TDLAT_3, TEX_2, MONOID_0, TOPMETR, TOPREAL1, PCOMPS_1, XXREAL_2, FUNCSDOM, CONVEX1, BINOP_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities TOPREAL1, EUCLID, COMPTS_1, SUBSET_1, STRUCT_0, ALGSTR_0, RLTOPSP1;
expansions TARSKI, TOPREAL1, COMPTS_1;
theorem
for
n,
k being
Nat st
n < k holds
n <= k - 1
theorem
for
n being
Nat for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL n) holds
( not
LSeg (
p1,
p2)
= LSeg (
q1,
q2) or (
p1 = q1 &
p2 = q2 ) or (
p1 = q2 &
p2 = q1 ) )
Lm1:
for P being Subset of (TOP-REAL 2) st not P is trivial & P is horizontal holds
not P is vertical
Lm2:
for f being FinSequence of the carrier of (TOP-REAL 2)
for k being Nat holds { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is finite
Lm3:
for f being FinSequence of the carrier of (TOP-REAL 2)
for k being Nat holds { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2)
Lm4:
for f being FinSequence of the carrier of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for k being Nat st Q = union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } holds
Q is closed
Lm5:
for f being FinSequence of the carrier of (TOP-REAL 2)
for i being Nat
for p1, p2 being Point of (TOP-REAL 2) st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds
ex p being Point of (TOP-REAL 2) st
( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )