defpred S1[ 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 & S1[x] ) )
from SUBSET_1:sch 1();
take
X
; 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; ( 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))) )
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; verum