defpred S₁[ set ] means ex l being Object of A st
( l = $1 & ( for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ) );
consider X being Subset of A such that
A1: for x being set holds
( x in X iff ( x in the carrier of A & S₁[x] ) ) from SUBSET_1:sch 1();
take X ; :: thesis: for o being Object of A holds
( o in X iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) )
let l be Object of A; :: thesis: ( l in X iff for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) )

hereby :: thesis: ( ( for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ) implies l in X )

assume l in X ; :: thesis: for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a)))
then S₁[l] by A1;
hence for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ; :: thesis: verum

end;

thus ( ( for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ) implies l in X ) by A1; :: thesis: verum