defpred S₁[ object ] means ex s being ManySortedFunction of X, the Sorts of C st
( s = $1 & (s . a) . x <> f );
consider S being set such that
A1: for x being object holds
( x in S iff ( x in C -States X & S₁[x] ) ) from XBOOLE_0:sch 1();
S c= C -States X by A1;
then reconsider S = S as Subset of (C -States X) ;
take S ; :: thesis: for s being ManySortedFunction of X, the Sorts of C holds
( s in S iff ( s in C -States X & (s . a) . x <> f ) )
let s be ManySortedFunction of X, the Sorts of C; :: thesis: ( s in S iff ( s in C -States X & (s . a) . x <> f ) )

hereby :: thesis: ( s in C -States X & (s . a) . x <> f implies s in S )

assume s in S ; :: thesis: ( s in C -States X & (s . a) . x <> f )
then ( s in C -States X & S₁[s] ) by A1;
hence ( s in C -States X & (s . a) . x <> f ) ; :: thesis: verum

end;

thus ( s in C -States X & (s . a) . x <> f implies s in S ) by A1; :: thesis: verum