{ (q `2) where q is Point of () : ( q `1 = E-bound (L~ g) & q in L~ g ) } c= REAL
proof
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in { (q `2) where q is Point of () : ( q `1 = E-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `2) where q is Point of () : ( q `1 = E-bound (L~ g) & q in L~ g ) } ; :: thesis:
then ex q being Point of () st
( X = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
hence X in REAL by XREAL_0:def 1; :: thesis: verum
end;
then reconsider B = { (q `2) where q is Point of () : ( q `1 = E-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
defpred S1[ Nat] means ( [(len (GoB g)),\$1] in Indices (GoB g) & ex i being Nat st
( i in dom g & g /. i = (GoB g) * ((len (GoB g)),\$1) ) );
set Y = { j where j is Element of NAT : S1[j] } ;
A61: { j where j is Element of NAT : S1[j] } c= Seg (width (GoB g))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in Seg (width (GoB g)) )
assume y in { j where j is Element of NAT : S1[j] } ; :: thesis: y in Seg (width (GoB g))
then ex j being Element of NAT st
( y = j & [(len (GoB g)),j] in Indices (GoB g) & ex i being Nat st
( i in dom g & g /. i = (GoB g) * ((len (GoB g)),j) ) ) ;
then [(len (GoB g)),y] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_0:def 4;
hence y in Seg (width (GoB g)) by ZFMISC_1:87; :: thesis: verum
end;
A62: { j where j is Element of NAT : S1[j] } is Subset of NAT from 0 <> len (GoB g) by MATRIX_0:def 10;
then 1 <= len (GoB g) by NAT_1:14;
then consider i, j being Nat such that
A63: i in dom g and
A64: [(len (GoB g)),j] in Indices (GoB g) and
A65: g /. i = (GoB g) * ((len (GoB g)),j) by Th7;
j in NAT by ORDINAL1:def 12;
then j in { j where j is Element of NAT : S1[j] } by ;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by ;
reconsider i1 = max Y as Nat by TARSKI:1;
set s1 = ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 ;
i1 in Y by XXREAL_2:def 8;
then consider j being Element of NAT such that
A66: j = i1 and
A67: [(len (GoB g)),j] in Indices (GoB g) and
A68: ex i being Nat st
( i in dom g & g /. i = (GoB g) * ((len (GoB g)),j) ) ;
A69: i1 <= width (GoB g) by ;
A70: 1 <= len (GoB g) by ;
1 <= i1 by ;
then A71: ((GoB g) * ((len (GoB g)),i1)) `1 = ((GoB g) * ((len (GoB g)),1)) `1 by ;
then A72: ((GoB g) * ((len (GoB g)),i1)) `1 = E-bound (L~ g) by Th39;
consider i being Nat such that
A73: i in dom g and
A74: g /. i = (GoB g) * ((len (GoB g)),j) by A68;
A75: i <= len g by ;
A76: 1 <= i by ;
A77: now :: thesis: ( ( i < len g & (GoB g) * ((len (GoB g)),i1) in L~ g ) or ( i = len g & (GoB g) * ((len (GoB g)),i1) in L~ g ) )
per cases ( i < len g or i = len g ) by ;
case i < len g ; :: thesis: (GoB g) * ((len (GoB g)),i1) in L~ g
then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg (g,i) by ;
hence (GoB g) * ((len (GoB g)),i1) in L~ g by ; :: thesis: verum
end;
case i = len g ; :: thesis: (GoB g) * ((len (GoB g)),i1) in L~ g
then g /. i in LSeg (g,(i -' 1)) by ;
hence (GoB g) * ((len (GoB g)),i1) in L~ g by ; :: thesis: verum
end;
end;
end;
((GoB g) * ((len (GoB g)),i1)) `1 = E-bound (L~ g) by ;
then A78: ((GoB g) * ((len (GoB g)),i1)) `2 in { (q `2) where q is Point of () : ( q `1 = E-bound (L~ g) & q in L~ g ) } by A77;
for r being Real st r in B holds
r <= ((GoB g) * ((len (GoB g)),i1)) `2
proof
let r be Real; :: thesis: ( r in B implies r <= ((GoB g) * ((len (GoB g)),i1)) `2 )
assume r in B ; :: thesis: r <= ((GoB g) * ((len (GoB g)),i1)) `2
then ex q being Point of () st
( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
hence r <= ((GoB g) * ((len (GoB g)),i1)) `2 by Lm4; :: thesis: verum
end;
then A79: upper_bound B <= ((GoB g) * ((len (GoB g)),i1)) `2 by ;
((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 is UpperBound of B
proof
let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in B or r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 )
assume r in B ; :: thesis: r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2
then A80: ex q being Point of () st
( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
1 <= len (GoB g) by GOBOARD7:32;
hence r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 by ; :: thesis: verum
end;
then B is bounded_above ;
then upper_bound B >= ((GoB g) * ((len (GoB g)),i1)) `2 by ;
then ((GoB g) * ((len (GoB g)),i1)) `2 = upper_bound B by
.= upper_bound (proj2 | (E-most (L~ g))) by Th14 ;
hence ex b1 being Nat st
( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-max (L~ g) ) by ; :: thesis: verum