theorem :: AOFA_000:111

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