defpred S₁[ Object of A] means for s being State of A
for a being Element of ObjectKind $1 holds Exec I,s = Exec I,(s +* $1,a);
let a, b be Subset of A; :: thesis: ( ( for o being Object of A holds
( o in a iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) ) ) & ( for o being Object of A holds
( o in b iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) ) ) 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