let f be non constant standard special_circular_sequence; :: thesis: (L~ f) ` = (LeftComp f) \/ (RightComp f)
union { (Cl (Down (Int (cell (GoB f),i,j)),((L~ f) ` ))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } c= (LeftComp f) \/ (RightComp f)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in union { (Cl (Down (Int (cell (GoB f),i,j)),((L~ f) ` ))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } or x in (LeftComp f) \/ (RightComp f) )
assume
x in union { (Cl (Down (Int (cell (GoB f),i,j)),((L~ f) ` ))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) }
;
:: thesis: x in (LeftComp f) \/ (RightComp f)
then consider y being
set such that A1:
(
x in y &
y in { (Cl (Down (Int (cell (GoB f),i,j)),((L~ f) ` ))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } )
by TARSKI:def 4;
consider i,
j being
Element of
NAT such that A2:
(
y = Cl (Down (Int (cell (GoB f),i,j)),((L~ f) ` )) &
i <= len (GoB f) &
j <= width (GoB f) )
by A1;
reconsider P =
Int (cell (GoB f),i,j) as
Subset of
(TOP-REAL 2) ;
reconsider Q =
(L~ f) ` as
Subset of
(TOP-REAL 2) ;
A3:
Cl (Down P,Q) = (Cl P) /\ Q
by A2, Th2, CONNSP_3:30;
A4:
Cl (Int (cell (GoB f),i,j)) c= Cl ((LeftComp f) \/ (RightComp f))
by A2, Th10, PRE_TOPC:49;
Cl ((LeftComp f) \/ (RightComp f)) = (Cl (LeftComp f)) \/ (Cl (RightComp f))
by PRE_TOPC:50;
then A5:
(Cl (Int (cell (GoB f),i,j))) /\ ((L~ f) ` ) c= ((Cl (LeftComp f)) \/ (Cl (RightComp f))) /\ ((L~ f) ` )
by A4, XBOOLE_1:26;
A6:
((Cl (LeftComp f)) \/ (Cl (RightComp f))) /\ ((L~ f) ` ) = ((Cl (LeftComp f)) /\ ((L~ f) ` )) \/ ((Cl (RightComp f)) /\ ((L~ f) ` ))
by XBOOLE_1:23;
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 &
B1 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) )
by CONNSP_1:def 6;
Cl B1 = (Cl (LeftComp f)) /\ ([#] ((TOP-REAL 2) | ((L~ f) ` )))
by A7, PRE_TOPC:47;
then A8:
Cl B1 = (Cl (LeftComp f)) /\ ((L~ f) ` )
by PRE_TOPC:def 10;
reconsider B1 =
B1 as
Subset of
((TOP-REAL 2) | ((L~ f) ` )) ;
B1 is
closed
by A7, CONNSP_1:35;
then A9:
(Cl (LeftComp f)) /\ ((L~ f) ` ) = LeftComp f
by A7, A8, PRE_TOPC:52;
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 A10:
(
B2 = RightComp f &
B2 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) )
by CONNSP_1:def 6;
Cl B2 = (Cl (RightComp f)) /\ ([#] ((TOP-REAL 2) | ((L~ f) ` )))
by A10, PRE_TOPC:47;
then A11:
Cl B2 = (Cl (RightComp f)) /\ ((L~ f) ` )
by PRE_TOPC:def 10;
reconsider B2 =
B2 as
Subset of
((TOP-REAL 2) | ((L~ f) ` )) ;
B2 is
closed
by A10, CONNSP_1:35;
then
(Cl (RightComp f)) /\ ((L~ f) ` ) = RightComp f
by A10, A11, PRE_TOPC:52;
hence
x in (LeftComp f) \/ (RightComp f)
by A1, A2, A3, A5, A6, A9;
:: thesis: verum
end;
then A12:
(L~ f) ` c= (LeftComp f) \/ (RightComp f)
by Th5;
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
A13:
( B1 = LeftComp f & B1 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) )
by CONNSP_1:def 6;
B1 c= the carrier of ((TOP-REAL 2) | ((L~ f) ` ))
;
then A14:
LeftComp f c= (L~ f) `
by A13, Lm1;
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
A15:
( B1 = RightComp f & B1 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) )
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 A14, A15, XBOOLE_1:8;
hence
(L~ f) ` = (LeftComp f) \/ (RightComp f)
by A12, XBOOLE_0:def 10; :: thesis: verum