begin
Lm1:
for f being non constant standard special_circular_sequence holds (L~ f) ` = the carrier of ((TOP-REAL 2) | ((L~ f) ` ))
Lm2:
the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:25;
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
Lm3:
for f being non constant standard special_circular_sequence holds
( Cl (Down (LeftComp f),((L~ f) ` )) is connected & Down (LeftComp f),((L~ f) ` ) = LeftComp f & Down (LeftComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) )
Lm4:
for f being non constant standard special_circular_sequence holds
( Cl (Down (RightComp f),((L~ f) ` )) is connected & Down (RightComp f),((L~ f) ` ) = RightComp f & Down (RightComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) )
theorem Th5:
theorem Th6:
Lm5:
for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Element of NAT st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 & Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) holds
Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f)
Lm6:
for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Element of NAT st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( j2 = j1 + 1 or j1 = j2 + 1 ) & i1 = i2 & Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) holds
Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f)
theorem Th7:
for
f being non
constant standard special_circular_sequence for
i1,
j1,
i2,
j2 being
Element of
NAT st
i1 <= len (GoB f) &
j1 <= width (GoB f) &
i2 <= len (GoB f) &
j2 <= width (GoB f) &
i1,
j1,
i2,
j2 are_adjacent2 holds
(
Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff
Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) )
theorem Th8:
theorem Th9:
theorem Th10:
theorem