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

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

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

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

A141: { 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

A143: i in dom g and

A144: [j,(width (GoB g))] in Indices (GoB g) and

A145: g /. i = (GoB g) * (j,(width (GoB g))) by Th8;

j in NAT by ORDINAL1:def 12;

then j in { j where j is Element of NAT : S_{1}[j] }
by A143, A144, A145;

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

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

set s1 = ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1 ;

i1 in Y by XXREAL_2:def 8;

then consider j being Element of NAT such that

A146: j = i1 and

A147: [j,(width (GoB g))] in Indices (GoB g) and

A148: ex i being Nat st

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

A149: i1 <= len (GoB g) by A146, A147, MATRIX_0:32;

A150: 1 <= width (GoB g) by A147, MATRIX_0:32;

1 <= i1 by A146, A147, MATRIX_0:32;

then A151: ((GoB g) * (i1,(width (GoB g)))) `2 = ((GoB g) * (1,(width (GoB g)))) `2 by A149, A150, GOBOARD5:1;

then A152: ((GoB g) * (i1,(width (GoB g)))) `2 = N-bound (L~ g) by Th40;

consider i being Nat such that

A153: i in dom g and

A154: g /. i = (GoB g) * (j,(width (GoB g))) by A148;

A155: i <= len g by A153, FINSEQ_3:25;

A156: 1 <= i by A153, FINSEQ_3:25;

then A158: ((GoB g) * (i1,(width (GoB g)))) `1 in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } by A157;

for r being Real st r in B holds

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

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

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

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

.= upper_bound (proj1 | (N-most (L~ g))) by Th15 ;

hence ex b_{1} being Nat st

( [b_{1},(width (GoB g))] in Indices (GoB g) & (GoB g) * (b_{1},(width (GoB g))) = N-max (L~ g) )
by A146, A147, A152, EUCLID:53; :: thesis: verum

proof

then reconsider B = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-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 = N-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 = N-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 = N-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 = N-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 = N-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,(width (GoB g))) ) );

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

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

proof

A142:
{ 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,(width (GoB g))] in Indices (GoB g) & ex i being Nat st

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

then [y,(width (GoB g))] 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,(width (GoB g))] in Indices (GoB g) & ex i being Nat st

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

then [y,(width (GoB g))] 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

A143: i in dom g and

A144: [j,(width (GoB g))] in Indices (GoB g) and

A145: g /. i = (GoB g) * (j,(width (GoB g))) 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)),(width (GoB g)))) `1 ;

i1 in Y by XXREAL_2:def 8;

then consider j being Element of NAT such that

A146: j = i1 and

A147: [j,(width (GoB g))] in Indices (GoB g) and

A148: ex i being Nat st

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

A149: i1 <= len (GoB g) by A146, A147, MATRIX_0:32;

A150: 1 <= width (GoB g) by A147, MATRIX_0:32;

1 <= i1 by A146, A147, MATRIX_0:32;

then A151: ((GoB g) * (i1,(width (GoB g)))) `2 = ((GoB g) * (1,(width (GoB g)))) `2 by A149, A150, GOBOARD5:1;

then A152: ((GoB g) * (i1,(width (GoB g)))) `2 = N-bound (L~ g) by Th40;

consider i being Nat such that

A153: i in dom g and

A154: g /. i = (GoB g) * (j,(width (GoB g))) by A148;

A155: i <= len g by A153, FINSEQ_3:25;

A156: 1 <= i by A153, FINSEQ_3:25;

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

((GoB g) * (i1,(width (GoB g)))) `2 = N-bound (L~ g)
by A151, Th40;end;

then A158: ((GoB g) * (i1,(width (GoB g)))) `1 in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } by A157;

for r being Real st r in B holds

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

proof

then A159:
upper_bound B <= ((GoB g) * (i1,(width (GoB g)))) `1
by A158, SEQ_4:45;
let r be Real; :: thesis: ( r in B implies r <= ((GoB g) * (i1,(width (GoB g)))) `1 )

assume r in B ; :: thesis: r <= ((GoB g) * (i1,(width (GoB g)))) `1

then ex q being Point of (TOP-REAL 2) st

( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ;

hence r <= ((GoB g) * (i1,(width (GoB g)))) `1 by Lm8; :: thesis: verum

end;assume r in B ; :: thesis: r <= ((GoB g) * (i1,(width (GoB g)))) `1

then ex q being Point of (TOP-REAL 2) st

( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ;

hence r <= ((GoB g) * (i1,(width (GoB g)))) `1 by Lm8; :: thesis: verum

((GoB g) * ((len (GoB g)),(width (GoB g)))) `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)),(width (GoB g)))) `1 )

assume r in B ; :: thesis: r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1

then A160: ex q being Point of (TOP-REAL 2) st

( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ;

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

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

end;assume r in B ; :: thesis: r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1

then A160: ex q being Point of (TOP-REAL 2) st

( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ;

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

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

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

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

.= upper_bound (proj1 | (N-most (L~ g))) by Th15 ;

hence ex b

( [b