environ
vocabularies HIDDEN, NUMBERS, RCOMP_1, SPPOL_1, SUBSET_1, EUCLID, RELAT_2, GOBOARD1, PRE_TOPC, FINSEQ_1, XBOOLE_0, FINSEQ_5, XXREAL_0, JORDAN3, RELAT_1, TOPREAL1, FUNCT_1, GROUP_2, ORDINAL4, ARYTM_3, TOPREAL2, PSCOMP_1, ARYTM_1, PARTFUN1, CARD_1, NAT_1, RLTOPSP1, MCART_1, SPRECT_2, FINSEQ_6, FINSEQ_4, ZFMISC_1, JORDAN1A, INT_1, JORDAN8, NEWTON, TARSKI, GOBOARD5, TREES_1, REAL_1, JORDAN2C, JORDAN9, JORDAN6, COMPLEX1, CONNSP_1, SEQ_4, XXREAL_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, COMPLEX1, INT_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, NEWTON, FINSEQ_5, MATRIX_0, ZFMISC_1, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPREAL2, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A;
definitions TARSKI;
theorems EUCLID, GOBRD11, JORDAN8, NEWTON, PSCOMP_1, JORDAN1A, NAT_1, TOPREAL6, GOBOARD5, NAT_2, FINSEQ_1, FINSEQ_2, JORDAN4, JORDAN6, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD9, SPPOL_1, SPPOL_2, REVROT_1, TOPREAL1, SPRECT_3, BOOLMARK, JORDAN3, JORDAN2C, SUBSET_1, JGRAPH_1, ABSVALUE, TOPREAL5, FINSEQ_3, XBOOLE_0, XBOOLE_1, PEPIN, XREAL_1, XXREAL_0, INT_1, NAT_D, ORDINAL1, XREAL_0, RLTOPSP1, MATRIX_0;
schemes ;
registrations XBOOLE_0, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, FINSEQ_5, STRUCT_0, MONOID_0, EUCLID, TOPREAL2, TOPREAL5, SPRECT_2, TOPREAL6, JORDAN8, FUNCT_1, RELAT_1, RLTOPSP1, SPPOL_2, JORDAN2C, ORDINAL1, NEWTON;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_D, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5, CONNSP_1, MONOID_0, GOBOARD1, PSCOMP_1, JORDAN3, JORDAN6, JORDAN2C, JORDAN8, JORDAN9, JORDAN1A, CONVEX1, RELSET_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities ;
expansions TARSKI;
Lm2:
for i, m being Nat st i <= m & m <= i + 1 & not i = m holds
i = m -' 1
Lm3:
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, n being Nat st j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i <> 0
Lm4:
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, n being Nat st i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j <> 0
Lm5:
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, n being Nat st j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i <> len (Gauge (C,n))
Lm6:
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, n being Nat st i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j <> width (Gauge (C,n))