defpred S₁[ Nat] means F . $1 = F . ($1 + 1);

hereby :: thesis: ( not F is halting implies ex b₁ being Element of NAT st b₁ = 0 )

assume F is halting ; :: thesis: ex IT being Element of NAT st
( S₁[IT] & ( for n being Nat st S₁[n] holds
IT <= n ) )
then A1: ex n being Nat st S₁[n] ;
ex IT being Nat st
( S₁[IT] & ( for n being Nat st S₁[n] holds
IT <= n ) ) from NAT_1:sch 5(A1);
then consider IT being Nat such that
A2: ( S₁[IT] & ( for n being Nat st S₁[n] holds
IT <= n ) ) ;
IT in NAT by ORDINAL1:def 12;
hence ex IT being Element of NAT st
( S₁[IT] & ( for n being Nat st S₁[n] holds
IT <= n ) ) by A2; :: thesis: verum

end;

thus ( not F is halting implies ex b₁ being Element of NAT st b₁ = 0 ) ; :: thesis: verum