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

defpred S_{1}[ Nat] means ( [$1,1] in Indices (GoB g) & ex i being Nat st

( i in dom g & g /. i = (GoB g) * ($1,1) ) );

set Y = { j where j is Element of NAT : S_{1}[j] } ;

A101: { j where j is Element of NAT : S_{1}[j] } c= dom (GoB g)
_{1}[j] } is Subset of NAT
from DOMAIN_1:sch 7();

1 <= width (GoB g) by GOBOARD7:33;

then consider i, j being 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 Th8;

j in NAT by ORDINAL1:def 12;

then j in { j where j is Element of NAT : S_{1}[j] }
by A103, A104, A105;

then reconsider Y = { j where j is Element of NAT : S_{1}[j] } as non empty finite Subset of NAT by A101, A102;

reconsider i1 = max Y as Nat by TARSKI:1;

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 Nat st

( i in dom g & g /. i = (GoB g) * (j,1) ) ;

A109: i1 <= len (GoB g) by A106, A107, MATRIX_0:32;

A110: 1 <= width (GoB g) by A107, MATRIX_0:32;

1 <= i1 by A106, A107, MATRIX_0:32;

then A111: ((GoB g) * (i1,1)) `2 = ((GoB g) * (1,1)) `2 by A109, A110, GOBOARD5:1;

then A112: ((GoB g) * (i1,1)) `2 = S-bound (L~ g) by Th38;

consider i being 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:25;

A116: 1 <= i by A113, FINSEQ_3:25;

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 st r in B holds

r <= ((GoB g) * (i1,1)) `1

((GoB g) * ((len (GoB g)),1)) `1 is UpperBound of B

then upper_bound B >= ((GoB g) * (i1,1)) `1 by A118, SEQ_4:def 1;

then ((GoB g) * (i1,1)) `1 = upper_bound B by A119, XXREAL_0:1

.= upper_bound (proj1 | (S-most (L~ g))) by Th16 ;

hence ex b_{1} being Nat st

( [b_{1},1] in Indices (GoB g) & (GoB g) * (b_{1},1) = S-max (L~ g) )
by A106, A107, A112, EUCLID:53; :: thesis: verum

proof

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 ;
let X be object ; :: 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 by XREAL_0:def 1; :: thesis: verum

end;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 by XREAL_0:def 1; :: thesis: verum

defpred S

( i in dom g & g /. i = (GoB g) * ($1,1) ) );

set Y = { j where j is Element of NAT : S

A101: { j where j is Element of NAT : S

proof

A102:
{ j where j is Element of NAT : S
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { j where j is Element of NAT : S_{1}[j] } or y in dom (GoB g) )

assume y in { j where j is Element of NAT : S_{1}[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 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_0:def 4;

hence y in dom (GoB g) by ZFMISC_1:87; :: thesis: verum

end;assume y in { j where j is Element of NAT : S

then ex j being Element of NAT st

( y = j & [j,1] in Indices (GoB g) & ex i being 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_0:def 4;

hence y in dom (GoB g) by ZFMISC_1:87; :: thesis: verum

1 <= width (GoB g) by GOBOARD7:33;

then consider i, j being 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 Th8;

j in NAT by ORDINAL1:def 12;

then j in { j where j is Element of NAT : S

then reconsider Y = { j where j is Element of NAT : S

reconsider i1 = max Y as Nat by TARSKI:1;

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 Nat st

( i in dom g & g /. i = (GoB g) * (j,1) ) ;

A109: i1 <= len (GoB g) by A106, A107, MATRIX_0:32;

A110: 1 <= width (GoB g) by A107, MATRIX_0:32;

1 <= i1 by A106, A107, MATRIX_0:32;

then A111: ((GoB g) * (i1,1)) `2 = ((GoB g) * (1,1)) `2 by A109, A110, GOBOARD5:1;

then A112: ((GoB g) * (i1,1)) `2 = S-bound (L~ g) by Th38;

consider i being 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:25;

A116: 1 <= i by A113, FINSEQ_3:25;

A117: now :: thesis: ( ( i < len g & (GoB g) * (i1,1) in L~ g ) or ( i = len g & (GoB g) * (i1,1) in L~ g ) )

((GoB g) * (i1,1)) `2 = S-bound (L~ g)
by A111, Th38;end;

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 st r in B holds

r <= ((GoB g) * (i1,1)) `1

proof

then A119:
upper_bound B <= ((GoB g) * (i1,1)) `1
by A118, SEQ_4:45;
let r be Real; :: 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;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

((GoB g) * ((len (GoB g)),1)) `1 is UpperBound of B

proof

then
B is bounded_above
;
let r be ExtReal; :: 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:33;

hence r <= ((GoB g) * ((len (GoB g)),1)) `1 by A120, Th32; :: thesis: verum

end;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:33;

hence r <= ((GoB g) * ((len (GoB g)),1)) `1 by A120, Th32; :: thesis: verum

then upper_bound B >= ((GoB g) * (i1,1)) `1 by A118, SEQ_4:def 1;

then ((GoB g) * (i1,1)) `1 = upper_bound B by A119, XXREAL_0:1

.= upper_bound (proj1 | (S-most (L~ g))) by Th16 ;

hence ex b

( [b