theorem :: AOFA_000:107

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
for P being set holds I is_terminating_wrt f,P by Th104, Th106;