theorem Th106: :: AOFA_000:106

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 Element of A st I is_terminating_wrt f holds
for P being set holds I is_terminating_wrt f,P ;