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

hereby :: thesis: ( 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 )

assume l in X ; :: thesis: ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a)
then S₁[l] by A4;
hence ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) ; :: thesis: verum

end;

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; :: thesis: verum