defpred S₁[ set ] means ex l being Object of A st
( l = $1 & ( for s being State of A
for a being Element of ObjectKind l holds Exec I,s = Exec I,(s +* l,a) ) );
consider X being Subset of A such that
A1: for x being set holds
( x in X iff ( x in the carrier of A & S₁[x] ) ) from SUBSET_1:sch 1();
take X ; :: thesis: for o being Object of A holds
( o in X iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) )
let l be Object of A; :: thesis: ( l in X iff for s being State of A
for a being Element of ObjectKind l holds Exec I,s = Exec I,(s +* l,a) )

hereby :: thesis: ( ( for s being State of A
for a being Element of ObjectKind l holds Exec I,s = Exec I,(s +* l,a) ) implies l in X )

assume l in X ; :: thesis: for s being State of A
for a being Element of ObjectKind l holds Exec I,s = Exec I,(s +* l,a)
then S₁[l] by A1;
hence for s being State of A
for a being Element of ObjectKind l holds Exec I,s = Exec I,(s +* l,a) ; :: thesis: verum

end;

thus ( ( for s being State of A
for a being Element of ObjectKind l holds Exec I,s = Exec I,(s +* l,a) ) implies l in X ) by A1; :: thesis: verum