defpred S1[ set ] means ex l being Object of A st
( l = $1 & ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) );
consider X being Subset of A such that
A4:
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 ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) )
let l be Object of A; ( l in X iff ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) )
thus
( ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) implies l in X )
by A4; verum