let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( f /. 1 = N-min (L~ f) implies LeftComp (SpStSeq (L~ f)) c= LeftComp f )
assume A1: f /. 1 = N-min (L~ f) ; :: thesis: LeftComp (SpStSeq (L~ f)) c= LeftComp f
A2: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
LeftComp (SpStSeq (L~ f)) is_a_component_of (L~ (SpStSeq (L~ f))) ` by GOBOARD9:def 1;
then consider B1 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq (L~ f))) ` )) such that
A3: B1 = LeftComp (SpStSeq (L~ f)) and
A4: B1 is_a_component_of (TOP-REAL 2) | ((L~ (SpStSeq (L~ f))) ` ) by CONNSP_1:def 6;
B1 is connected by A4, CONNSP_1:def 5;
then A5: LeftComp (SpStSeq (L~ f)) is connected by A3, CONNSP_1:24;
consider i being Element of NAT such that
A6: ( 1 <= i & i < len (GoB f) ) and
A7: N-min (L~ f) = (GoB f) * i,(width (GoB f)) by Th45;
A8: i in dom (GoB f) by A6, FINSEQ_3:27;
then A9: f /. 2 = (GoB f) * (i + 1),(width (GoB f)) by A1, A7, Th46;
A10: width (GoB f) >= 1 by GOBRD11:34;
then A11: ((width (GoB f)) -' 1) + 1 = width (GoB f) by XREAL_1:237;
A12: 1 + 1 <= len f by GOBOARD7:36, XXREAL_0:2;
A13: [i,(width (GoB f))] in Indices (GoB f) by A6, A10, MATRIX_1:37;
A14: ( 1 <= i + 1 & i + 1 <= len (GoB f) ) by A6, NAT_1:13;
then [(i + 1),(width (GoB f))] in Indices (GoB f) by A10, MATRIX_1:37;
then A15: left_cell f,1 = cell (GoB f),i,(width (GoB f)) by A1, A7, A9, A11, A12, A13, GOBOARD5:29;
set a = ((1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))))) + |[0 ,1]|;
set q = (1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))));
A16: ((1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))))) + |[0 ,1]| in Int (cell (GoB f),i,(width (GoB f))) by A6, A14, GOBOARD6:35;
A17: Int (cell (GoB f),i,(width (GoB f))) c= LeftComp f by A15, GOBOARD9:def 1;
A18: (((1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))))) + |[0 ,1]|) `2 = (((1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))))) `2 ) + (|[0 ,1]| `2 ) by TOPREAL3:7
.= (((1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))))) `2 ) + 1 by EUCLID:56 ;
A19: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:68;
A20: (f /. 2) `2 = ((GoB f) * 1,(width (GoB f))) `2 by A9, A10, A14, GOBOARD5:2
.= (N-min (L~ f)) `2 by A6, A7, A10, GOBOARD5:2
.= N-bound (L~ f) by EUCLID:56 ;
A21: LeftComp (SpStSeq (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ (SpStSeq (L~ f))) <= p `1 or not p `1 <= E-bound (L~ (SpStSeq (L~ f))) or not S-bound (L~ (SpStSeq (L~ f))) <= p `2 or not p `2 <= N-bound (L~ (SpStSeq (L~ f))) ) } by Th54;
((1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))))) `2 = ((1 / 2) * (((GoB f) * i,(width (GoB f))) + (f /. 2))) `2 by A1, A7, A8, Th46
.= (1 / 2) * (((f /. 1) + (f /. 2)) `2 ) by A1, A7, TOPREAL3:9
.= (1 / 2) * (((f /. 1) `2 ) + ((f /. 2) `2 )) by TOPREAL3:7
.= (1 / 2) * ((N-bound (L~ f)) + (N-bound (L~ f))) by A1, A20, EUCLID:56
.= N-bound (L~ f) ;
then (((1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))))) + |[0 ,1]|) `2 > 0 + (N-bound (L~ f)) by A18, XREAL_1:10;
then (((1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))))) + |[0 ,1]|) `2 > N-bound (L~ (SpStSeq (L~ f))) by SPRECT_1:68;
then ((1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))))) + |[0 ,1]| in LeftComp (SpStSeq (L~ f)) by A21;
then A22: LeftComp f meets LeftComp (SpStSeq (L~ f)) by A16, A17, XBOOLE_0:3;
defpred S₁[ Element of (TOP-REAL 2)] means $1 `2 < S-bound (L~ f);
reconsider P1 = { p where p is Point of (TOP-REAL 2) : S<sub>1</sub>[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
defpred S<sub>2</sub>[ Element of (TOP-REAL 2)] means $1 `2 > N-bound (L~ f);
reconsider P2 = { p where p is Point of (TOP-REAL 2) : S₂[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
defpred S₃[ Element of (TOP-REAL 2)] means $1 `1 > E-bound (L~ f);
reconsider P3 = { p where p is Point of (TOP-REAL 2) : S<sub>3</sub>[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
defpred S<sub>4</sub>[ Element of (TOP-REAL 2)] means $1 `1 < W-bound (L~ f);
reconsider P4 = { p where p is Point of (TOP-REAL 2) : S₄[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
A23: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:66;
A24: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:67;
A25: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:69;
A26: LeftComp (SpStSeq (L~ f)) = (P1 \/ P2) \/ (P3 \/ P4)

proof

thus LeftComp (SpStSeq (L~ f)) c= (P1 \/ P2) \/ (P3 \/ P4) :: according to XBOOLE_0:def 10 :: thesis: (P1 \/ P2) \/ (P3 \/ P4) c= LeftComp (SpStSeq (L~ f))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LeftComp (SpStSeq (L~ f)) or x in (P1 \/ P2) \/ (P3 \/ P4) )
assume x in LeftComp (SpStSeq (L~ f)) ; :: thesis: x in (P1 \/ P2) \/ (P3 \/ P4)
then x in { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } by A19, A23, A24, A25, Th54;
then ex p being Point of (TOP-REAL 2) st
( p = x & ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) ) ;
then ( x in P1 or x in P2 or x in P3 or x in P4 ) ;
then ( x in P1 \/ P2 or x in P3 \/ P4 ) by XBOOLE_0:def 3;
hence x in (P1 \/ P2) \/ (P3 \/ P4) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (P1 \/ P2) \/ (P3 \/ P4) or x in LeftComp (SpStSeq (L~ f)) )
assume x in (P1 \/ P2) \/ (P3 \/ P4) ; :: thesis: x in LeftComp (SpStSeq (L~ f))
then A27: ( x in P1 \/ P2 or x in P3 \/ P4 ) by XBOOLE_0:def 3;

per cases ( x in P1 or x in P2 or x in P3 or x in P4 ) by A27, XBOOLE_0:def 3;

suppose x in P1 ; :: thesis: x in LeftComp (SpStSeq (L~ f))

then ex p being Point of (TOP-REAL 2) st
( x = p & p `2 < S-bound (L~ f) ) ;
hence x in LeftComp (SpStSeq (L~ f)) by A24, Th57; :: thesis: verum

end;

suppose x in P2 ; :: thesis: x in LeftComp (SpStSeq (L~ f))

then ex p being Point of (TOP-REAL 2) st
( x = p & p `2 > N-bound (L~ f) ) ;
hence x in LeftComp (SpStSeq (L~ f)) by A19, Th57; :: thesis: verum

end;

suppose x in P3 ; :: thesis: x in LeftComp (SpStSeq (L~ f))

then ex p being Point of (TOP-REAL 2) st
( x = p & p `1 > E-bound (L~ f) ) ;
hence x in LeftComp (SpStSeq (L~ f)) by A25, Th57; :: thesis: verum

end;

suppose x in P4 ; :: thesis: x in LeftComp (SpStSeq (L~ f))

then ex p being Point of (TOP-REAL 2) st
( x = p & p `1 < W-bound (L~ f) ) ;
hence x in LeftComp (SpStSeq (L~ f)) by A23, Th57; :: thesis: verum

end;

end;

end;

for p being Point of (TOP-REAL 2) st p in P1 holds
p `2 < ((GoB f) * 1,1) `2

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in P1 implies p `2 < ((GoB f) * 1,1) `2 )
assume p in P1 ; :: thesis: p `2 < ((GoB f) * 1,1) `2
then ex q being Point of (TOP-REAL 2) st
( p = q & q `2 < S-bound (L~ f) ) ;
hence p `2 < ((GoB f) * 1,1) `2 by JORDAN5D:40; :: thesis: verum

end;

then A28: P1 misses L~ f by GOBOARD8:23;
for p being Point of (TOP-REAL 2) st p in P2 holds
p `2 > ((GoB f) * 1,(width (GoB f))) `2

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in P2 implies p `2 > ((GoB f) * 1,(width (GoB f))) `2 )
assume p in P2 ; :: thesis: p `2 > ((GoB f) * 1,(width (GoB f))) `2
then ex q being Point of (TOP-REAL 2) st
( p = q & q `2 > N-bound (L~ f) ) ;
hence p `2 > ((GoB f) * 1,(width (GoB f))) `2 by JORDAN5D:42; :: thesis: verum

end;

then P2 misses L~ f by GOBOARD8:24;
then A29: P1 \/ P2 misses L~ f by A28, XBOOLE_1:70;
for p being Point of (TOP-REAL 2) st p in P3 holds
p `1 > ((GoB f) * (len (GoB f)),1) `1

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in P3 implies p `1 > ((GoB f) * (len (GoB f)),1) `1 )
assume p in P3 ; :: thesis: p `1 > ((GoB f) * (len (GoB f)),1) `1
then ex q being Point of (TOP-REAL 2) st
( p = q & q `1 > E-bound (L~ f) ) ;
hence p `1 > ((GoB f) * (len (GoB f)),1) `1 by JORDAN5D:41; :: thesis: verum

end;

then A30: P3 misses L~ f by GOBOARD8:22;
for p being Point of (TOP-REAL 2) st p in P4 holds
p `1 < ((GoB f) * 1,1) `1

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in P4 implies p `1 < ((GoB f) * 1,1) `1 )
assume p in P4 ; :: thesis: p `1 < ((GoB f) * 1,1) `1
then ex q being Point of (TOP-REAL 2) st
( p = q & q `1 < W-bound (L~ f) ) ;
hence p `1 < ((GoB f) * 1,1) `1 by JORDAN5D:39; :: thesis: verum

end;

then P4 misses L~ f by GOBOARD8:21;
then P3 \/ P4 misses L~ f by A30, XBOOLE_1:70;
then LeftComp (SpStSeq (L~ f)) misses L~ f by A26, A29, XBOOLE_1:70;
then LeftComp (SpStSeq (L~ f)) c= (L~ f) ` by SUBSET_1:43;
hence LeftComp (SpStSeq (L~ f)) c= LeftComp f by A2, A5, A22, GOBOARD9:6; :: thesis: verum