let S be non empty set ; :: according to AOFA_000:def 36 :: thesis: for s being Element of S
for T being Subset of S
for f being ExecutionFunction of A,S,T holds [s,(if-then-else C,I,J)] in TerminatingPrograms A,S,T,f
let s be Element of S; :: thesis: for T being Subset of S
for f being ExecutionFunction of A,S,T holds [s,(if-then-else C,I,J)] in TerminatingPrograms A,S,T,f
let T be Subset of S; :: thesis: for f being ExecutionFunction of A,S,T holds [s,(if-then-else C,I,J)] in TerminatingPrograms A,S,T,f
let f be ExecutionFunction of A,S,T; :: thesis: [s,(if-then-else C,I,J)] in TerminatingPrograms A,S,T,f
( [s,C] in TerminatingPrograms A,S,T,f & ( f . s,C in T or f . s,C nin T ) & [(f . s,C),I] in TerminatingPrograms A,S,T,f & [(f . s,C),J] in TerminatingPrograms A,S,T,f ) by Def36;
hence [s,(if-then-else C,I,J)] in TerminatingPrograms A,S,T,f by Def35; :: thesis: verum