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