let I be Program of SCM+FSA ; :: thesis: ( I is parahalting implies I is InitHalting )
assume I is parahalting ; :: thesis: I is InitHalting
then reconsider I = I as parahalting Program of SCM+FSA ;
Initialized I is halting ;
hence I is InitHalting by Def2; :: thesis: verum