{ (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } c= REAL
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))
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;
((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
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
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; verum