environ
vocabularies HIDDEN, NUMBERS, FUNCT_1, GOBOARD5, SUBSET_1, REAL_1, PRE_TOPC, EUCLID, GOBOARD1, CONNSP_1, XBOOLE_0, RELAT_1, STRUCT_0, TARSKI, RELAT_2, RLTOPSP1, CONVEX1, FINSEQ_1, FINSEQ_5, ARYTM_3, ARYTM_1, XXREAL_0, PARTFUN1, MCART_1, GOBOARD2, CARD_1, MATRIX_1, COMPLEX1, TREES_1, TOPS_1, TOPREAL1, GOBOARD9, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, MATRIX_0, SEQ_4, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, FINSEQ_5, GOBOARD5, XXREAL_0;
definitions TARSKI, GOBOARD5, GOBOARD1, JORDAN1, XBOOLE_0, SEQM_3;
theorems CONNSP_1, GOBOARD5, TOPS_1, SPPOL_2, PRE_TOPC, GOBOARD1, TARSKI, TOPREAL1, GOBOARD2, FINSEQ_3, NAT_1, SUBSET_1, FINSEQ_6, GOBOARD6, GOBOARD7, GOBOARD8, FINSEQ_1, FINSEQ_5, JORDAN1, TSEP_1, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, PARTFUN1, MATRIX_0, NAT_D, SEQM_3, SEQ_4, XREAL_0;
schemes NAT_1;
registrations RELSET_1, NUMBERS, XXREAL_0, FINSEQ_1, FINSEQ_6, STRUCT_0, PRE_TOPC, EUCLID, GOBOARD2, GOBOARD5, ORDINAL1, RLTOPSP1, JORDAN1, XREAL_0, INT_1;
constructors HIDDEN, REAL_1, FINSEQ_5, TOPS_1, CONNSP_1, GOBOARD2, GOBOARD5, GOBOARD1, NAT_D, RELSET_1, CONVEX1, RVSUM_1, SEQ_4;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities GOBOARD5, XBOOLE_0, STRUCT_0;
expansions GOBOARD1, XBOOLE_0;
Lm1:
for f, ff being non empty FinSequence of (TOP-REAL 2) st ff = Rev f holds
GoB ff = GoB f
definition
let f be non
constant standard special_circular_sequence;
A1:
1
+ 1
< len f
by GOBOARD7:34, XXREAL_0:2;
then A2:
Int (left_cell (f,1)) <> {}
by Th14;
A3:
Int (right_cell (f,1)) <> {}
by A1, Th15;
existence
ex b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b1 )
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st b1 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b1 & b2 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b2 holds
b1 = b2
by A2, Th1, XBOOLE_1:67;
existence
ex b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b1 )
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st b1 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b1 & b2 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b2 holds
b1 = b2
by A3, Th1, XBOOLE_1:67;
end;