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