set n = ApproxIndex C;
defpred S₁[ Nat] means ( $1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),$1) c= BDD C );
set X = { i where i is Element of NAT : S₁[i] } ;
A1: { i where i is Element of NAT : S₁[i] } is Subset of NAT from DOMAIN_1:sch 7();
ApproxIndex C is_sufficiently_large_for C by Def1;
then consider j being Nat such that
A2: S₁[j] ;
A3: j in NAT by ORDINAL1:def 12;
j in { i where i is Element of NAT : S₁[i] } by A2, A3;
then reconsider X = { i where i is Element of NAT : S₁[i] } as non empty Subset of NAT by A1;
take min X ; :: thesis: ( min X < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(min X)) c= BDD C & ( for j being Nat st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= min X ) )
min X in X by XXREAL_2:def 7;
then ex i being Element of NAT st
( i = min X & S₁[i] ) ;
hence S₁[ min X] ; :: thesis: for j being Nat st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= min X
let i be Nat; :: thesis: ( i < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),i) c= BDD C implies i >= min X )
A4: i in NAT by ORDINAL1:def 12;
assume S₁[i] ; :: thesis: i >= min X
then i in X by A4;
hence i >= min X by XXREAL_2:def 7; :: thesis: verum