let A be preIfWhileAlgebra; :: thesis: 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
let S be non empty set ; :: thesis: 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
let T be Subset of S; :: thesis: for f being ExecutionFunction of A,S,T
for I being Element of A holds S is_invariant_wrt I,f
let f be ExecutionFunction of A,S,T; :: thesis: for I being Element of A holds S is_invariant_wrt I,f
let I be Element of A; :: thesis: S is_invariant_wrt I,f
let s be Element of S; :: according to AOFA_000:def 39 :: thesis: ( s in S implies f . s,I in S )
thus ( s in S implies f . s,I in S ) ; :: thesis: verum