for A being preIfWhileAlgebra
for S being non empty set
for T being Subset of S
for f being ExecutionFunction of A,S,T
for I being absolutely-terminating Element of A holds I is_terminating_wrt f by Def36;