defpred S_{1}[ 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_{1}[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 ) )

( 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

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 )

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

then ( s in C -States X & S_{1}[s] )
by A1;

hence ( s in C -States X & (s . a) . x <> f ) ; :: thesis: verum

end;then ( s in C -States X & S

hence ( s in C -States X & (s . a) . x <> f ) ; :: thesis: verum