environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, ORDERS_2, SUBSET_1, RELAT_2, FIN_TOPO, TARSKI, CONNSP_1, PRE_TOPC, STRUCT_0, RELAT_1, RCOMP_1, FINSEQ_1, ORDINAL2, XXREAL_0, NAT_1, ARYTM_3, FUNCT_1, ORDINAL4, PARTFUN1, CARD_1, ARYTM_1, BORSUK_2, RFINSEQ, FINTOPO3, FINTOPO6;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, XXREAL_0, NAT_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, STRUCT_0, ORDERS_2, FIN_TOPO, FINTOPO3, NAT_D, ENUMSET1, FINTOPO4, PRE_TOPC, RFINSEQ;
definitions TARSKI, XBOOLE_0, FIN_TOPO;
theorems NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, RELSET_1, XBOOLE_0, XBOOLE_1, FIN_TOPO, FINTOPO3, ENUMSET1, FINTOPO4, FINSEQ_6, JORDAN4, TARSKI, XREAL_1, SUBSET_1, PRE_TOPC, RFINSEQ, FINSEQ_3, FINSEQ_5, REVROT_1, ORDINAL1, XXREAL_0, PARTFUN1, XREAL_0, NAT_D;
schemes NAT_1, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, FIN_TOPO, ORDINAL1;
constructors HIDDEN, DOMAIN_1, EQREL_1, RFINSEQ, RFUNCT_3, NAT_D, FIN_TOPO, FINTOPO3, FINTOPO4, REAL_1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, SUBSET_1, FIN_TOPO, FINSEQ_1;
expansions TARSKI, XBOOLE_0, FIN_TOPO;
Lm1:
for T being RelStr holds RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T
Lm2:
for FT being non empty RelStr
for x being Element of FT holds <*x*> is continuous
by FINSEQ_1:39;
Lm3:
for FT being non empty RelStr
for x being Element of FT holds {x} is arcwise_connected
Lm4:
for FT being non empty RelStr
for f being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds
ex g being FinSequence of FT st
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) )