{ (q `1 ) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } c= REAL

proof

let X be set ; :: according to TARSKI:def 3 :: thesis: ( not X in { (q `1 ) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `1 ) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } ; :: thesis: X in REAL
then ex q being Point of (TOP-REAL 2) st
( X = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ;
hence X in REAL ; :: thesis: verum

end;

then reconsider B = { (q `1 ) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
defpred S₁[ Element of NAT ] means ( [$1,1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * $1,1 ) );
set Y = { j where j is Element of NAT : S₁[j] } ;
A101: { j where j is Element of NAT : S₁[j] } c= dom (GoB g)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { j where j is Element of NAT : S₁[j] } or y in dom (GoB g) )
assume y in { j where j is Element of NAT : S₁[j] } ; :: thesis: y in dom (GoB g)
then ex j being Element of NAT st
( y = j & [j,1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * j,1 ) ) ;
then [y,1] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def 5;
hence y in dom (GoB g) by ZFMISC_1:106; :: thesis: verum

end;

A102: { j where j is Element of NAT : S₁[j] } is Subset of NAT from DOMAIN_1:sch 7();
1 <= width (GoB g) by GOBOARD7:35;
then consider i, j being Element of NAT such that
A103: i in dom g and
A104: [j,1] in Indices (GoB g) and
A105: g /. i = (GoB g) * j,1 by Th10;
j in { j where j is Element of NAT : S₁[j] } by A103, A104, A105;
then reconsider Y = { j where j is Element of NAT : S₁[j] } as non empty finite Subset of NAT by A101, A102;
reconsider i1 = max Y as Element of NAT by ORDINAL1:def 13;
set s1 = ((GoB g) * (len (GoB g)),1) `1 ;
i1 in Y by XXREAL_2:def 8;
then consider j being Element of NAT such that
A106: j = i1 and
A107: [j,1] in Indices (GoB g) and
A108: ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * j,1 ) ;
A109: i1 <= len (GoB g) by A106, A107, MATRIX_1:39;
A110: 1 <= width (GoB g) by A107, MATRIX_1:39;
1 <= i1 by A106, A107, MATRIX_1:39;
then A111: ((GoB g) * i1,1) `2 = ((GoB g) * 1,1) `2 by A109, A110, GOBOARD5:2;
then A112: ((GoB g) * i1,1) `2 = S-bound (L~ g) by Th40;
consider i being Element of NAT such that
A113: i in dom g and
A114: g /. i = (GoB g) * j,1 by A108;
A115: i <= len g by A113, FINSEQ_3:27;
A116: 1 <= i by A113, FINSEQ_3:27;

A117: now

per cases ( i < len g or i = len g ) by A115, XXREAL_0:1;

case i < len g ; :: thesis: (GoB g) * i1,1 in L~ g

then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg g,i by A116, TOPREAL1:27;
hence (GoB g) * i1,1 in L~ g by A106, A114, SPPOL_2:17; :: thesis: verum

end;

case i = len g ; :: thesis: (GoB g) * i1,1 in L~ g

then g /. i in LSeg g,(i -' 1) by Lm9, Th3;
hence (GoB g) * i1,1 in L~ g by A106, A114, SPPOL_2:17; :: thesis: verum

end;

end;

end;

((GoB g) * i1,1) `2 = S-bound (L~ g) by A111, Th40;
then A118: ((GoB g) * i1,1) `1 in { (q `1 ) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } by A117;
for r being real number st r in B holds
r <= ((GoB g) * i1,1) `1

proof

let r be real number ; :: thesis: ( r in B implies r <= ((GoB g) * i1,1) `1 )
assume r in B ; :: thesis: r <= ((GoB g) * i1,1) `1
then ex q being Point of (TOP-REAL 2) st
( r = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ;
hence r <= ((GoB g) * i1,1) `1 by Lm7; :: thesis: verum

end;

then A119: upper_bound B <= ((GoB g) * i1,1) `1 by A118, SEQ_4:62;
((GoB g) * (len (GoB g)),1) `1 is UpperBound of B

proof

let r be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not r in B or r <= ((GoB g) * (len (GoB g)),1) `1 )
assume r in B ; :: thesis: r <= ((GoB g) * (len (GoB g)),1) `1
then A120: ex q being Point of (TOP-REAL 2) st
( r = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ;
1 <= width (GoB g) by GOBOARD7:35;
hence r <= ((GoB g) * (len (GoB g)),1) `1 by A120, Th34; :: thesis: verum

end;

then B is bounded_above by XXREAL_2:def 10;
then upper_bound B >= ((GoB g) * i1,1) `1 by A118, SEQ_4:def 4;
then ((GoB g) * i1,1) `1 = upper_bound B by A119, XXREAL_0:1
.= upper_bound (proj1 | (S-most (L~ g))) by Th18 ;
hence ex b₁ being Element of NAT st
( [b₁,1] in Indices (GoB g) & (GoB g) * b₁,1 = S-max (L~ g) ) by A106, A107, A112, EUCLID:57; :: thesis: verum