defpred S₁[ Nat] means A in (Seq_of_ind T) . $1;
A1: ex n being Nat st S₁[n] by B1, Def2;
consider MIN being Nat such that
A2: S₁[MIN] and
A3: for n being Nat st S₁[n] holds
MIN <= n from NAT_1:sch 5(A1);
take I = MIN - 1; :: thesis: ( A in (Seq_of_ind T) . (I + 1) & not A in (Seq_of_ind T) . I )

now :: thesis: not A in (Seq_of_ind T) . I

assume A4: A in (Seq_of_ind T) . I ; :: thesis: contradiction
then I in dom (Seq_of_ind T) by FUNCT_1:def 2;
then reconsider i = I as Element of NAT ;
MIN <= i by A3, A4;
then MIN < i + 1 by NAT_1:13;
hence contradiction ; :: thesis: verum

end;

hence ( A in (Seq_of_ind T) . (I + 1) & not A in (Seq_of_ind T) . I ) by A2; :: thesis: verum