{ (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-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 (TOP-REAL 2) : ( q `1 = W-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 = W-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 = W-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 (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
set s1 = ((GoB g) * (1,1)) `2 ;
defpred S1[ 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 : S1[j] } ;
A1: { 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 & [1,j] in Indices (GoB g) & ex i being Nat st
( i in dom g & g /. i = (GoB g) * (1,j) ) ) ;
then [1,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;
A2: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch 7();
 A3: 1 <= len (GoB g) by GOBOARD7:32;
then consider i, j being Nat such that
A4: i in dom g and
A5: [1,j] in Indices (GoB g) and
A6: g /. i = (GoB g) * (1,j) by Th7;
j in NAT by ORDINAL1:def 12;
then j in { j where j is Element of NAT : S1[j] } by A4, A5, A6;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A1, A2;
set i1 = min Y;
min Y in Y by XXREAL_2:def 7;
then consider j being Element of NAT such that
A7: j = min Y and
A8: [1,j] in Indices (GoB g) and
A9: ex i being Nat st
( i in dom g & g /. i = (GoB g) * (1,j) ) ;
A10: min Y <= width (GoB g) by A7, A8, MATRIX_0:32;
A11: 1 <= len (GoB g) by A8, MATRIX_0:32;
1 <= min Y by A7, A8, MATRIX_0:32;
then A12: ((GoB g) * (1,(min Y))) `1 = ((GoB g) * (1,1)) `1 by A11, A10, GOBOARD5:2;
then A13: ((GoB g) * (1,(min Y))) `1 = W-bound (L~ g) by Th37;
consider i being Nat such that
A14: i in dom g and
A15: g /. i = (GoB g) * (1,j) by A9;
A16: i <= len g by A14, FINSEQ_3:25;
A17: 1 <= i by A14, FINSEQ_3:25;
A18: now :: thesis: ( ( i < len g & (GoB g) * (1,(min Y)) in L~ g ) or ( i = len g & (GoB g) * (1,(min Y)) in L~ g ) )
per cases ( i < len g or i = len g ) by A16, XXREAL_0:1;
case i < len g ; :: thesis: (GoB g) * (1,(min Y)) in L~ g
then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg (g,i) by A17, TOPREAL1:21;
hence (GoB g) * (1,(min Y)) in L~ g by A7, A15, SPPOL_2:17; :: thesis: verum
end;
case i = len g ; :: thesis: (GoB g) * (1,(min Y)) in L~ g
then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1;
hence (GoB g) * (1,(min Y)) in L~ g by A7, A15, SPPOL_2:17; :: thesis: verum
end;
end;
end;
((GoB g) * (1,(min Y))) `1 = W-bound (L~ g) by A12, Th37;
then A19: ((GoB g) * (1,(min Y))) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } by A18;
for r being Real st r in B holds
r >= ((GoB g) * (1,(min Y))) `2
proof
let r be Real; :: thesis: ( r in B implies r >= ((GoB g) * (1,(min Y))) `2 )
assume r in B ; :: thesis: r >= ((GoB g) * (1,(min Y))) `2
then ex q being Point of (TOP-REAL 2) st
( r = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ;
hence r >= ((GoB g) * (1,(min Y))) `2 by Lm1; :: thesis: verum
end;
then A20: lower_bound B >= ((GoB g) * (1,(min Y))) `2 by A19, SEQ_4:43;
((GoB g) * (1,1)) `2 is LowerBound of B
proof
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in B or ((GoB g) * (1,1)) `2 <= r )
assume r in B ; :: thesis: ((GoB g) * (1,1)) `2 <= r
then ex q being Point of (TOP-REAL 2) st
( r = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ;
hence ((GoB g) * (1,1)) `2 <= r by A3, Th33; :: thesis: verum
end;
then B is bounded_below ;
then lower_bound B <= ((GoB g) * (1,(min Y))) `2 by A19, SEQ_4:def 2;
then ((GoB g) * (1,(min Y))) `2 = lower_bound B by A20, XXREAL_0:1
.= lower_bound (proj2 | (W-most (L~ g))) by Th13 ;
hence ex b1 being Nat st
( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-min (L~ g) ) by A7, A8, A13, EUCLID:53; :: thesis: verum