environ
vocabularies HIDDEN, NUMBERS, TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, GOBOARD1, SUBSET_1, FINSEQ_1, ARYTM_3, XXREAL_0, FINSEQ_6, RELAT_1, PARTFUN1, FINSEQ_4, CARD_1, ORDINAL4, RFINSEQ, NAT_1, GRAPH_2, MATRIX_1, ARYTM_1, FINSEQ_5, EUCLID, RLTOPSP1, TOPREAL1, GOBOARD5, STRUCT_0, MCART_1, SETFAM_1, PRE_TOPC;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, SETFAM_1, FUNCT_1, PARTFUN1, FINSEQ_5, FINSEQ_6, RFINSEQ, GRAPH_2, MATRIX_0, RELSET_1, FINSEQ_1, ZFMISC_1, STRUCT_0, PRE_TOPC, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD5, FINSEQ_4, XXREAL_0;
definitions FINSEQ_6, GOBOARD1, GOBOARD5, TOPREAL1, TARSKI;
theorems GRAPH_2, FINSEQ_3, NAT_1, FINSEQ_5, TOPREAL1, FINSEQ_1, TARSKI, FUNCT_1, FINSEQ_4, ZFMISC_1, PARTFUN2, FINSEQ_6, RELAT_1, RFINSEQ, INT_1, MSSCYC_1, REVROT_1, GOBOARD2, TOPREAL3, GOBOARD3, SPPOL_2, GOBOARD5, GOBOARD7, ENUMSET1, SETFAM_1, XBOOLE_0, XBOOLE_1, XREAL_1, CARD_1, XXREAL_0, PARTFUN1, NAT_D, SEQM_3;
schemes ;
registrations XBOOLE_0, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, FINSEQ_5, FINSEQ_6, STRUCT_0, SPPOL_2, GOBOARD9, SPRECT_1, REVROT_1, CARD_1, FUNCT_1, RELAT_1, EUCLID;
constructors HIDDEN, SETFAM_1, REAL_1, FINSEQ_4, RFINSEQ, NAT_D, FINSEQ_5, REALSET2, GOBOARD1, GOBOARD5, GRAPH_2, SPRECT_1, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities TOPREAL1;
expansions GOBOARD1, TOPREAL1, TARSKI;
theorem Th1:
for
A,
x,
y being
set st
A c= {x,y} &
x in A & not
y in A holds
A = {x}
Lm1:
for p being FinSequence
for m, n being Nat st 1 <= m & m <= n + 1 & n <= len p holds
( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
Lm2:
for f being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for g being non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being Nat st i < len f & 1 < i holds
for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> f /. 1
Lm3:
for f being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for g being non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being Nat st j > len f & j + 1 < len (f ^' g) holds
for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> g /. (len g)