let F be NAT -defined the InstructionsF of S -valued Function; :: thesis: ( F is 0 -halting implies F is parahalting )
assume A2: F is 0 -halting ; :: thesis: F is parahalting
let s be 0 -started State of S; :: according to AMISTD_1:def 11 :: thesis: for b₁ being set holds
( not F c= b₁ or b₁ halts_on s )
thus for b₁ being set holds
( not F c= b₁ or b₁ halts_on s ) by A2, Def7; :: thesis: verum