defpred S₁[ set ] means ex s being State of A st s . $1 <> (Exec (I,s)) . $1;
let a, b be Subset of A; :: thesis: ( ( for o being Object of A holds
( o in a iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) & ( for o being Object of A holds
( o in b iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) implies a = b )
assume that
A2: for o being Object of A holds
( o in a iff S₁[o] ) and
A3: for o being Object of A holds
( o in b iff S₁[o] ) ; :: thesis: a = b
thus a = b from SUBSET_1:sch 2(A2, A3); :: thesis: verum