let h be non constant standard special_circular_sequence; :: thesis:
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 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

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ; :: thesis:
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:

end;

reconsider a = a as Point of (TOP-REAL 2) by A1;
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;
upper_bound X = ((GoB h) * (1,(width (GoB h)))) `2

let p be Real; :: thesis:
assume p in X ; :: thesis:
then ex s being Point of (TOP-REAL 2) st
( p = s `2 & s in L~ h ) ;
hence p <= ((GoB h) * (1,(width (GoB h)))) `2 by A3, Th34; :: thesis:

end;

1 <= width (GoB h) by GOBOARD7:33;
then consider q1 being Point of (TOP-REAL 2) such that
A5: q1 `2 = ((GoB h) * (1,(width (GoB h)))) `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,(width (GoB h)))) `2 <= q

A7: q11 in X by A6;
let q be Real; :: thesis:
assume for p being Real st p in X holds
p <= q ; :: thesis:
hence ((GoB h) * (1,(width (GoB h)))) `2 <= q by A5, A7; :: thesis:

end;

end;

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