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

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

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] } ;

A81: { 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();

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

then consider i, j being Nat such that

A84: i in dom g and

A85: [j,1] in Indices (GoB g) and

A86: 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 A84, A85, A86;

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

set i1 = min Y;

min Y in Y by XXREAL_2:def 7;

then consider j being Element of NAT such that

A87: j = min Y and

A88: [j,1] in Indices (GoB g) and

A89: ex i being Nat st

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

A90: min Y <= len (GoB g) by A87, A88, MATRIX_0:32;

A91: 1 <= width (GoB g) by A88, MATRIX_0:32;

1 <= min Y by A87, A88, MATRIX_0:32;

then A92: ((GoB g) * ((min Y),1)) `2 = ((GoB g) * (1,1)) `2 by A90, A91, GOBOARD5:1;

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

consider i being Nat such that

A94: i in dom g and

A95: g /. i = (GoB g) * (j,1) by A89;

A96: i <= len g by A94, FINSEQ_3:25;

A97: 1 <= i by A94, FINSEQ_3:25;

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

for r being Real st r in B holds

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

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

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

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

.= lower_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-min (L~ g) )
by A87, A88, A93, 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

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

defpred S

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

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

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

proof

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

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

then consider i, j being Nat such that

A84: i in dom g and

A85: [j,1] in Indices (GoB g) and

A86: 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

set i1 = min Y;

min Y in Y by XXREAL_2:def 7;

then consider j being Element of NAT such that

A87: j = min Y and

A88: [j,1] in Indices (GoB g) and

A89: ex i being Nat st

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

A90: min Y <= len (GoB g) by A87, A88, MATRIX_0:32;

A91: 1 <= width (GoB g) by A88, MATRIX_0:32;

1 <= min Y by A87, A88, MATRIX_0:32;

then A92: ((GoB g) * ((min Y),1)) `2 = ((GoB g) * (1,1)) `2 by A90, A91, GOBOARD5:1;

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

consider i being Nat such that

A94: i in dom g and

A95: g /. i = (GoB g) * (j,1) by A89;

A96: i <= len g by A94, FINSEQ_3:25;

A97: 1 <= i by A94, FINSEQ_3:25;

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

((GoB g) * ((min Y),1)) `2 = S-bound (L~ g)
by A92, Th38;end;

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

for r being Real st r in B holds

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

proof

then A100:
lower_bound B >= ((GoB g) * ((min Y),1)) `1
by A99, SEQ_4:43;
let r be Real; :: thesis: ( r in B implies r >= ((GoB g) * ((min Y),1)) `1 )

assume r in B ; :: thesis: r >= ((GoB g) * ((min Y),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) * ((min Y),1)) `1 by Lm5; :: thesis: verum

end;assume r in B ; :: thesis: r >= ((GoB g) * ((min Y),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) * ((min Y),1)) `1 by Lm5; :: thesis: verum

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

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

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

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

hence ((GoB g) * (1,1)) `1 <= r by A83, Th31; :: thesis: verum

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

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

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

hence ((GoB g) * (1,1)) `1 <= r by A83, Th31; :: thesis: verum

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

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

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

hence ex b

( [b