defpred S₁[ Object of A] means ex s being State of A ex a being Element of ObjectKind $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 ObjectKind 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 ObjectKind 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