defpred S₁[ Object of A] means ex s being State of A ex a being Element of Values $1 st Exec (I,(s +* ($1,a))) <> (Exec (I,s)) +* ($1,a);
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 ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) ) & ( for o being Object of A holds
( o in b 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) ) ) implies a = b )
assume that
A5: for o being Object of A holds
( o in a iff S₁[o] ) and
A6: for o being Object of A holds
( o in b iff S₁[o] ) ; :: thesis: a = b
thus a = b from SUBSET_1:sch 2(A5, A6); :: thesis: verum