{ (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } c= REAL
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 ;
defpred S1[ 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 : S1[j] } ;
A121:
{ j where j is Element of NAT : S1[j] } c= dom (GoB g)
A122:
{ j where j is Element of NAT : S1[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
A123:
i in dom g
and
A124:
[j,(width (GoB g))] in Indices (GoB g)
and
A125:
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 : S1[j] }
by A123, A124, A125;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A121, A122;
set i1 = min Y;
set s1 = ((GoB g) * (1,(width (GoB g)))) `1 ;
min Y in Y
by XXREAL_2:def 7;
then consider j being Element of NAT such that
A126:
j = min Y
and
A127:
[j,(width (GoB g))] in Indices (GoB g)
and
A128:
ex i being Nat st
( i in dom g & g /. i = (GoB g) * (j,(width (GoB g))) )
;
A129:
min Y <= len (GoB g)
by A126, A127, MATRIX_0:32;
A130:
1 <= width (GoB g)
by A127, MATRIX_0:32;
1 <= min Y
by A126, A127, MATRIX_0:32;
then A131:
((GoB g) * ((min Y),(width (GoB g)))) `2 = ((GoB g) * (1,(width (GoB g)))) `2
by A129, A130, GOBOARD5:1;
then A132:
((GoB g) * ((min Y),(width (GoB g)))) `2 = N-bound (L~ g)
by Th40;
consider i being Nat such that
A133:
i in dom g
and
A134:
g /. i = (GoB g) * (j,(width (GoB g)))
by A128;
A135:
i <= len g
by A133, FINSEQ_3:25;
A136:
1 <= i
by A133, FINSEQ_3:25;
((GoB g) * ((min Y),(width (GoB g)))) `2 = N-bound (L~ g)
by A131, Th40;
then A138:
((GoB g) * ((min Y),(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 A137;
for r being Real st r in B holds
r >= ((GoB g) * ((min Y),(width (GoB g)))) `1
then A139:
lower_bound B >= ((GoB g) * ((min Y),(width (GoB g)))) `1
by A138, SEQ_4:43;
((GoB g) * (1,(width (GoB g)))) `1 is LowerBound of B
then
B is bounded_below
;
then
lower_bound B <= ((GoB g) * ((min Y),(width (GoB g)))) `1
by A138, SEQ_4:def 2;
then ((GoB g) * ((min Y),(width (GoB g)))) `1 =
lower_bound B
by A139, XXREAL_0:1
.=
lower_bound (proj1 | (N-most (L~ g)))
by Th15
;
hence
ex b1 being Nat st
( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-min (L~ g) )
by A126, A127, A132, EUCLID:53; verum