:: The First Part of Jordan's Theorem for Special Polygons
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Copyright (c) 1996-2019 Association of Mizar Users

Lm1: for f being non constant standard special_circular_sequence holds (L~ f)  = the carrier of (() | ((L~ f) ))
proof end;

Lm2: the carrier of () = REAL 2
by EUCLID:22;

theorem Th1: :: GOBRD12:1
for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
Int (cell ((GoB f),i,j)) c= (L~ f)  by ;

theorem Th2: :: GOBRD12:2
for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) ))) = (cell ((GoB f),i,j)) /\ ((L~ f) )
proof end;

theorem Th3: :: GOBRD12:3
for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
( Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) ))) is connected & Down ((Int (cell ((GoB f),i,j))),((L~ f) )) = Int (cell ((GoB f),i,j)) )
proof end;

Lm3: for f being non constant standard special_circular_sequence holds
( Cl (Down ((),((L~ f) ))) is connected & Down ((),((L~ f) )) = LeftComp f & Down ((),((L~ f) )) is a_component )

proof end;

Lm4: for f being non constant standard special_circular_sequence holds
( Cl (Down ((),((L~ f) ))) is connected & Down ((),((L~ f) )) = RightComp f & Down ((),((L~ f) )) is a_component )

proof end;

theorem Th4: :: GOBRD12:4
for f being non constant standard special_circular_sequence holds (L~ f)  = union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) )))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }
proof end;

theorem Th5: :: GOBRD12:5
for f being non constant standard special_circular_sequence holds
( (Down ((),((L~ f) ))) \/ (Down ((),((L~ f) ))) is a_union_of_components of () | ((L~ f) ) & Down ((),((L~ f) )) = LeftComp f & Down ((),((L~ f) )) = RightComp f )
proof end;

Lm5: for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being 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= () \/ () holds
Int (cell ((GoB f),i2,j2)) c= () \/ ()

proof end;

Lm6: for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being 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= () \/ () holds
Int (cell ((GoB f),i2,j2)) c= () \/ ()

proof end;

theorem Th6: :: GOBRD12:6
for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Nat st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent holds
( Int (cell ((GoB f),i1,j1)) c= () \/ () iff Int (cell ((GoB f),i2,j2)) c= () \/ () )
proof end;

theorem Th7: :: GOBRD12:7
for f being non constant standard special_circular_sequence
for F1, F2 being FinSequence of NAT st len F1 = len F2 & ex i being Nat st
( i in dom F1 & Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= () \/ () ) & ( for i, k1, k2 being Nat st i in dom F1 & k1 = F1 . i & k2 = F2 . i holds
( k1 <= len (GoB f) & k2 <= width (GoB f) ) ) holds
for i being Nat st i in dom F1 holds
Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= () \/ ()
proof end;

theorem Th8: :: GOBRD12:8
for f being non constant standard special_circular_sequence ex i, j being Nat st
( i <= len (GoB f) & j <= width (GoB f) & Int (cell ((GoB f),i,j)) c= () \/ () )
proof end;

theorem Th9: :: GOBRD12:9
for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
Int (cell ((GoB f),i,j)) c= () \/ ()
proof end;

:: Jordan Curve Theorem for special polygons
theorem :: GOBRD12:10
for f being non constant standard special_circular_sequence holds (L~ f) ` = () \/ ()
proof end;