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

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

defpred S_{1}[ 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 : S_{1}[j] } ;

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

A43: 1 <= len (GoB g) by GOBOARD7:32;

then consider i, j being Nat such that

A44: i in dom g and

A45: [(len (GoB g)),j] in Indices (GoB g) and

A46: 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 : S_{1}[j] }
by A44, A45, A46;

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

set i1 = min Y;

min Y in Y by XXREAL_2:def 7;

then consider j being Element of NAT such that

A47: j = min Y and

A48: [(len (GoB g)),j] in Indices (GoB g) and

A49: ex i being Nat st

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

A50: min Y <= width (GoB g) by A47, A48, MATRIX_0:32;

A51: 1 <= len (GoB g) by A48, MATRIX_0:32;

1 <= min Y by A47, A48, MATRIX_0:32;

then A52: ((GoB g) * ((len (GoB g)),(min Y))) `1 = ((GoB g) * ((len (GoB g)),1)) `1 by A51, A50, GOBOARD5:2;

then A53: ((GoB g) * ((len (GoB g)),(min Y))) `1 = E-bound (L~ g) by Th39;

consider i being Nat such that

A54: i in dom g and

A55: g /. i = (GoB g) * ((len (GoB g)),j) by A49;

A56: i <= len g by A54, FINSEQ_3:25;

A57: 1 <= i by A54, FINSEQ_3:25;

then A59: ((GoB g) * ((len (GoB g)),(min Y))) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } by A58;

for r being Real st r in B holds

r >= ((GoB g) * ((len (GoB g)),(min Y))) `2

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

then lower_bound B <= ((GoB g) * ((len (GoB g)),(min Y))) `2 by A59, SEQ_4:def 2;

then ((GoB g) * ((len (GoB g)),(min Y))) `2 = lower_bound B by A60, XXREAL_0:1

.= lower_bound (proj2 | (E-most (L~ g))) by Th14 ;

hence ex b_{1} being Nat st

( [(len (GoB g)),b_{1}] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b_{1}) = E-min (L~ g) )
by A47, A48, A53, EUCLID:53; :: thesis: verum

proof

then reconsider B = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-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 `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } or X in REAL )

assume X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } ; :: thesis: X in REAL

then ex q being Point of (TOP-REAL 2) 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;assume X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } ; :: thesis: X in REAL

then ex q being Point of (TOP-REAL 2) 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

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

defpred S

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

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

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

proof

A42:
{ 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 Seg (width (GoB g)) )

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

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

A43: 1 <= len (GoB g) by GOBOARD7:32;

then consider i, j being Nat such that

A44: i in dom g and

A45: [(len (GoB g)),j] in Indices (GoB g) and

A46: 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 : S

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

set i1 = min Y;

min Y in Y by XXREAL_2:def 7;

then consider j being Element of NAT such that

A47: j = min Y and

A48: [(len (GoB g)),j] in Indices (GoB g) and

A49: ex i being Nat st

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

A50: min Y <= width (GoB g) by A47, A48, MATRIX_0:32;

A51: 1 <= len (GoB g) by A48, MATRIX_0:32;

1 <= min Y by A47, A48, MATRIX_0:32;

then A52: ((GoB g) * ((len (GoB g)),(min Y))) `1 = ((GoB g) * ((len (GoB g)),1)) `1 by A51, A50, GOBOARD5:2;

then A53: ((GoB g) * ((len (GoB g)),(min Y))) `1 = E-bound (L~ g) by Th39;

consider i being Nat such that

A54: i in dom g and

A55: g /. i = (GoB g) * ((len (GoB g)),j) by A49;

A56: i <= len g by A54, FINSEQ_3:25;

A57: 1 <= i by A54, FINSEQ_3:25;

A58: now :: thesis: ( ( i < len g & (GoB g) * ((len (GoB g)),(min Y)) in L~ g ) or ( i = len g & (GoB g) * ((len (GoB g)),(min Y)) in L~ g ) )end;

((GoB g) * ((len (GoB g)),(min Y))) `1 = E-bound (L~ g)
by A52, Th39;per cases
( i < len g or i = len g )
by A56, XXREAL_0:1;

end;

then A59: ((GoB g) * ((len (GoB g)),(min Y))) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } by A58;

for r being Real st r in B holds

r >= ((GoB g) * ((len (GoB g)),(min Y))) `2

proof

then A60:
lower_bound B >= ((GoB g) * ((len (GoB g)),(min Y))) `2
by A59, SEQ_4:43;
let r be Real; :: thesis: ( r in B implies r >= ((GoB g) * ((len (GoB g)),(min Y))) `2 )

assume r in B ; :: thesis: r >= ((GoB g) * ((len (GoB g)),(min Y))) `2

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

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

hence r >= ((GoB g) * ((len (GoB g)),(min Y))) `2 by Lm3; :: thesis: verum

end;assume r in B ; :: thesis: r >= ((GoB g) * ((len (GoB g)),(min Y))) `2

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

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

hence r >= ((GoB g) * ((len (GoB g)),(min Y))) `2 by Lm3; :: thesis: verum

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

proof

then
B is bounded_below
;
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in B or ((GoB g) * ((len (GoB g)),1)) `2 <= r )

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

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

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

hence ((GoB g) * ((len (GoB g)),1)) `2 <= r by A43, Th33; :: thesis: verum

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

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

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

hence ((GoB g) * ((len (GoB g)),1)) `2 <= r by A43, Th33; :: thesis: verum

then lower_bound B <= ((GoB g) * ((len (GoB g)),(min Y))) `2 by A59, SEQ_4:def 2;

then ((GoB g) * ((len (GoB g)),(min Y))) `2 = lower_bound B by A60, XXREAL_0:1

.= lower_bound (proj2 | (E-most (L~ g))) by Th14 ;

hence ex b

( [(len (GoB g)),b