let f be non constant standard special_circular_sequence; (L~ f) ` = (LeftComp f) \/ (RightComp f)
LeftComp f is_a_component_of (L~ f) `
by GOBOARD9:def 1;
then consider B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that
A1:
B1 = LeftComp f
and
B1 is a_component
by CONNSP_1:def 6;
B1 c= the carrier of ((TOP-REAL 2) | ((L~ f) `))
;
then A2:
LeftComp f c= (L~ f) `
by A1, Lm1;
union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } c= (LeftComp f) \/ (RightComp f)
proof
RightComp f is_a_component_of (L~ f) `
by GOBOARD9:def 2;
then consider B2 being
Subset of
((TOP-REAL 2) | ((L~ f) `)) such that A3:
B2 = RightComp f
and A4:
B2 is
a_component
by CONNSP_1:def 6;
Cl B2 = (Cl (RightComp f)) /\ ([#] ((TOP-REAL 2) | ((L~ f) `)))
by A3, PRE_TOPC:17;
then A5:
Cl B2 = (Cl (RightComp f)) /\ ((L~ f) `)
by PRE_TOPC:def 5;
reconsider B2 =
B2 as
Subset of
((TOP-REAL 2) | ((L~ f) `)) ;
B2 is
closed
by A4, CONNSP_1:33;
then A6:
(Cl (RightComp f)) /\ ((L~ f) `) = RightComp f
by A3, A5, PRE_TOPC:22;
LeftComp f is_a_component_of (L~ f) `
by GOBOARD9:def 1;
then consider B1 being
Subset of
((TOP-REAL 2) | ((L~ f) `)) such that A7:
B1 = LeftComp f
and A8:
B1 is
a_component
by CONNSP_1:def 6;
Cl B1 = (Cl (LeftComp f)) /\ ([#] ((TOP-REAL 2) | ((L~ f) `)))
by A7, PRE_TOPC:17;
then A9:
Cl B1 = (Cl (LeftComp f)) /\ ((L~ f) `)
by PRE_TOPC:def 5;
reconsider B1 =
B1 as
Subset of
((TOP-REAL 2) | ((L~ f) `)) ;
B1 is
closed
by A8, CONNSP_1:33;
then A10:
(
((Cl (LeftComp f)) \/ (Cl (RightComp f))) /\ ((L~ f) `) = ((Cl (LeftComp f)) /\ ((L~ f) `)) \/ ((Cl (RightComp f)) /\ ((L~ f) `)) &
(Cl (LeftComp f)) /\ ((L~ f) `) = LeftComp f )
by A7, A9, PRE_TOPC:22, XBOOLE_1:23;
reconsider Q =
(L~ f) ` as
Subset of
(TOP-REAL 2) ;
let x be
object ;
TARSKI:def 3 ( not x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } or x in (LeftComp f) \/ (RightComp f) )
A11:
Cl ((LeftComp f) \/ (RightComp f)) = (Cl (LeftComp f)) \/ (Cl (RightComp f))
by PRE_TOPC:20;
assume
x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }
;
x in (LeftComp f) \/ (RightComp f)
then consider y being
set such that A12:
(
x in y &
y in { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } )
by TARSKI:def 4;
consider i,
j being
Nat such that A13:
y = Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))
and A14:
(
i <= len (GoB f) &
j <= width (GoB f) )
by A12;
Cl (Int (cell ((GoB f),i,j))) c= Cl ((LeftComp f) \/ (RightComp f))
by A14, Th9, PRE_TOPC:19;
then A15:
(Cl (Int (cell ((GoB f),i,j)))) /\ ((L~ f) `) c= ((Cl (LeftComp f)) \/ (Cl (RightComp f))) /\ ((L~ f) `)
by A11, XBOOLE_1:26;
reconsider P =
Int (cell ((GoB f),i,j)) as
Subset of
(TOP-REAL 2) ;
Cl (Down (P,Q)) = (Cl P) /\ Q
by A14, Th1, CONNSP_3:29;
hence
x in (LeftComp f) \/ (RightComp f)
by A12, A13, A15, A10, A6;
verum
end;
then A16:
(L~ f) ` c= (LeftComp f) \/ (RightComp f)
by Th4;
RightComp f is_a_component_of (L~ f) `
by GOBOARD9:def 2;
then consider B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that
A17:
B1 = RightComp f
and
B1 is a_component
by CONNSP_1:def 6;
B1 c= the carrier of ((TOP-REAL 2) | ((L~ f) `))
;
then
B1 c= (L~ f) `
by Lm1;
then
(LeftComp f) \/ (RightComp f) c= (L~ f) `
by A2, A17, XBOOLE_1:8;
hence
(L~ f) ` = (LeftComp f) \/ (RightComp f)
by A16, XBOOLE_0:def 10; verum