:: deftheorem defines is_invariant_wrt AOFA_000:def 39 :
for A being preIfWhileAlgebra
for S being non empty set
for T being Subset of S
for I being Element of A
for f being ExecutionFunction of A,S,T
for Z being set holds
( Z is_invariant_wrt I,f iff for s being Element of S st s in Z holds
f . (s,I) in Z );