defpred S₁[ set ] means ex s being State of A st s . $1 <> (Exec (I,s)) . $1;
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 ex s being State of A st s . o <> (Exec (I,s)) . o )
thus for o being Object of A holds
( o in X iff ex s being State of A st s . o <> (Exec (I,s)) . o ) by A1; :: thesis: verum