defpred S₁[ Nat] means G c= (Seq_of_ind T) . $1;
A2: ex n being Nat st S₁[n] by A1;
consider MIN being Nat such that
A3: S₁[MIN] and
A4: for n being Nat st S₁[n] holds
MIN <= n from NAT_1:sch 5(A2);
take I = MIN - 1; :: thesis: ( G c= (Seq_of_ind T) . (I + 1) & - 1 <= I & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I <= i ) )

A5: now :: thesis: for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I <= i

let i be Integer; :: thesis: ( - 1 <= i & G c= (Seq_of_ind T) . (i + 1) implies I <= i )
assume that
A6: - 1 <= i and
A7: G c= (Seq_of_ind T) . (i + 1) ; :: thesis: I <= i
(- 1) + 1 <= i + 1 by A6, XREAL_1:6;
then i + 1 in NAT by INT_1:3;
then reconsider I1 = i + 1 as Nat ;
( MIN = I + 1 & MIN <= I1 ) by A4, A7;
hence I <= i by XREAL_1:6; :: thesis: verum

end;

I >= 0 - 1 by XREAL_1:9;
hence ( G c= (Seq_of_ind T) . (I + 1) & - 1 <= I & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I <= i ) ) by A3, A5; :: thesis: verum