let h be non constant standard special_circular_sequence; :: thesis: N-bound (L~ h) = ((GoB h) * 1,(width (GoB h))) `2
set X = { (q `2 ) where q is Point of (TOP-REAL 2) : q in L~ h } ;
set A = ((GoB h) * 1,(width (GoB h))) `2 ;
consider a being set such that
A1: a in L~ h by XBOOLE_0:def 1;
reconsider a = a as Point of (TOP-REAL 2) by A1;
A2: a `2 in { (q `2 ) where q is Point of (TOP-REAL 2) : q in L~ h } by A1;
{ (q `2 ) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL

proof

let b be set ; :: 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 consider qq being Point of (TOP-REAL 2) such that
A3: ( b = qq `2 & qq in L~ h ) ;
thus b in REAL by A3; :: thesis: verum

end;

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;
upper_bound X = ((GoB h) * 1,(width (GoB h))) `2

proof

A4: ( 1 <= len (GoB h) & 1 <= width (GoB h) ) by GOBOARD7:34, GOBOARD7:35;
A5: for p being real number st p in X holds
p <= ((GoB h) * 1,(width (GoB h))) `2

proof

let p be real number ; :: thesis: ( p in X implies p <= ((GoB h) * 1,(width (GoB h))) `2 )
assume p in X ; :: thesis: p <= ((GoB h) * 1,(width (GoB h))) `2
then consider s being Point of (TOP-REAL 2) such that
A6: ( p = s `2 & s in L~ h ) ;
thus p <= ((GoB h) * 1,(width (GoB h))) `2 by A4, A6, Th36; :: thesis: verum

end;

consider q1 being Point of (TOP-REAL 2) such that
A7: ( q1 `2 = ((GoB h) * 1,(width (GoB h))) `2 & q1 in L~ h ) by A4, Th38;
reconsider q11 = q1 `2 as Real ;
for q being real number st ( for p being real number st p in X holds
p <= q ) holds
((GoB h) * 1,(width (GoB h))) `2 <= q

proof

let q be real number ; :: thesis: ( ( for p being real number st p in X holds
p <= q ) implies ((GoB h) * 1,(width (GoB h))) `2 <= q )
assume A8: for p being real number st p in X holds
p <= q ; :: thesis: ((GoB h) * 1,(width (GoB h))) `2 <= q
q11 in X by A7;
hence ((GoB h) * 1,(width (GoB h))) `2 <= q by A7, A8; :: thesis: verum

end;

hence upper_bound X = ((GoB h) * 1,(width (GoB h))) `2 by A5, SEQ_4:63; :: thesis: verum

end;

hence N-bound (L~ h) = ((GoB h) * 1,(width (GoB h))) `2 by Th20; :: thesis: verum