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 holds S is_invariant_wrt I,f ;