let S be non empty set ; :: thesis:
let T be Subset of S; :: thesis:
let A be free ECIW-strict preIfWhileAlgebra; :: thesis:
let f1, f2 be ExecutionFunction of A,S,T; :: thesis:
assume A1: f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] ; :: thesis:
set TP1 = TerminatingPrograms (A,S,T,f1);
set TP2 = TerminatingPrograms (A,S,T,f2);
thus TerminatingPrograms (A,S,T,f1) c= TerminatingPrograms (A,S,T,f2) :: according to XBOOLE_0:def 10 :: thesis:

let q, I be object ; :: according to RELAT_1:def 3 :: thesis:
assume A2: [q,I] in TerminatingPrograms (A,S,T,f1) ; :: thesis:
then A3: q is Element of S by ZFMISC_1:87;
I is Element of A by A2, ZFMISC_1:87;
hence not [q,I] nin TerminatingPrograms (A,S,T,f2) by A1, A2, A3, Lm3; :: thesis:

end;

let q, I be object ; :: according to RELAT_1:def 3 :: thesis:
assume A4: [q,I] in TerminatingPrograms (A,S,T,f2) ; :: thesis:
then A5: q is Element of S by ZFMISC_1:87;
I is Element of A by A4, ZFMISC_1:87;
hence not [q,I] nin TerminatingPrograms (A,S,T,f1) by A1, A4, A5, Lm3; :: thesis: