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