let h be non constant standard special_circular_sequence; :: thesis: S-bound (L~ h) = ((GoB h) * (1,1)) `2

set X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ;

set A = ((GoB h) * (1,1)) `2 ;

consider a being object such that

A1: a in L~ h by XBOOLE_0:def 1;

A2: { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL

a `2 in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } by A1;

then reconsider X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } as non empty Subset of REAL by A2;

lower_bound X = ((GoB h) * (1,1)) `2

set X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ;

set A = ((GoB h) * (1,1)) `2 ;

consider a being object such that

A1: a in L~ h by XBOOLE_0:def 1;

A2: { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL

proof

reconsider a = a as Point of (TOP-REAL 2) by A1;
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } or b in REAL )

assume b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ; :: thesis: b in REAL

then ex qq being Point of (TOP-REAL 2) st

( b = qq `2 & qq in L~ h ) ;

hence b in REAL by XREAL_0:def 1; :: thesis: verum

end;assume b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ; :: thesis: b in REAL

then ex qq being Point of (TOP-REAL 2) st

( b = qq `2 & qq in L~ h ) ;

hence b in REAL by XREAL_0:def 1; :: thesis: verum

a `2 in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } by A1;

then reconsider X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } as non empty Subset of REAL by A2;

lower_bound X = ((GoB h) * (1,1)) `2

proof

hence
S-bound (L~ h) = ((GoB h) * (1,1)) `2
by Th18; :: thesis: verum
A3:
1 <= len (GoB h)
by GOBOARD7:32;

A4: for p being Real st p in X holds

p >= ((GoB h) * (1,1)) `2

then consider q1 being Point of (TOP-REAL 2) such that

A5: q1 `2 = ((GoB h) * (1,1)) `2 and

A6: q1 in L~ h by A3, Th36;

reconsider q11 = q1 `2 as Real ;

for q being Real st ( for p being Real st p in X holds

p >= q ) holds

((GoB h) * (1,1)) `2 >= q

end;A4: for p being Real st p in X holds

p >= ((GoB h) * (1,1)) `2

proof

1 <= width (GoB h)
by GOBOARD7:33;
let p be Real; :: thesis: ( p in X implies p >= ((GoB h) * (1,1)) `2 )

assume p in X ; :: thesis: p >= ((GoB h) * (1,1)) `2

then ex s being Point of (TOP-REAL 2) st

( p = s `2 & s in L~ h ) ;

hence p >= ((GoB h) * (1,1)) `2 by A3, Th33; :: thesis: verum

end;assume p in X ; :: thesis: p >= ((GoB h) * (1,1)) `2

then ex s being Point of (TOP-REAL 2) st

( p = s `2 & s in L~ h ) ;

hence p >= ((GoB h) * (1,1)) `2 by A3, Th33; :: thesis: verum

then consider q1 being Point of (TOP-REAL 2) such that

A5: q1 `2 = ((GoB h) * (1,1)) `2 and

A6: q1 in L~ h by A3, Th36;

reconsider q11 = q1 `2 as Real ;

for q being Real st ( for p being Real st p in X holds

p >= q ) holds

((GoB h) * (1,1)) `2 >= q

proof

hence
lower_bound X = ((GoB h) * (1,1)) `2
by A4, SEQ_4:44; :: thesis: verum
A7:
q11 in X
by A6;

let q be Real; :: thesis: ( ( for p being Real st p in X holds

p >= q ) implies ((GoB h) * (1,1)) `2 >= q )

assume for p being Real st p in X holds

p >= q ; :: thesis: ((GoB h) * (1,1)) `2 >= q

hence ((GoB h) * (1,1)) `2 >= q by A5, A7; :: thesis: verum

end;let q be Real; :: thesis: ( ( for p being Real st p in X holds

p >= q ) implies ((GoB h) * (1,1)) `2 >= q )

assume for p being Real st p in X holds

p >= q ; :: thesis: ((GoB h) * (1,1)) `2 >= q

hence ((GoB h) * (1,1)) `2 >= q by A5, A7; :: thesis: verum