let A be preIfWhileAlgebra; :: thesis: for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T holds [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f
let S be non empty set ; :: thesis: for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T holds [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f
let T be Subset of S; :: thesis: for s being Element of S
for f being ExecutionFunction of A,S,T holds [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T holds [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f
let f be ExecutionFunction of A,S,T; :: thesis: [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f
set I = EmptyIns A;
EmptyIns A in {(EmptyIns A)} by TARSKI:def 1;
then A1: [s,(EmptyIns A)] in [:S,{(EmptyIns A)}:] by ZFMISC_1:106;
[:S,{(EmptyIns A)}:] c= TerminatingPrograms A,S,T,f by Def35;
hence [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f by A1; :: thesis: verum