begin
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 Th15;
A3:
Int (right_cell (f,1)) <> {}
by A1, Th16;
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;