let S1, S2 be Subset of (C -States X); :: thesis: ( ( for s being ManySortedFunction of X, the Sorts of C holds

( s in S1 iff ( s in C -States X & (s . a) . x <> f ) ) ) & ( for s being ManySortedFunction of X, the Sorts of C holds

( s in S2 iff ( s in C -States X & (s . a) . x <> f ) ) ) implies S1 = S2 )

assume that

A2: for s being ManySortedFunction of X, the Sorts of C holds

( s in S1 iff ( s in C -States X & (s . a) . x <> f ) ) and

A3: for s being ManySortedFunction of X, the Sorts of C holds

( s in S2 iff ( s in C -States X & (s . a) . x <> f ) ) ; :: thesis: S1 = S2

thus S1 c= S2 :: according to XBOOLE_0:def 10 :: thesis: S2 c= S1

assume A5: c in S2 ; :: thesis: c in S1

then reconsider s = c as ManySortedFunction of X, the Sorts of C by Th43;

( s in C -States X & (s . a) . x <> f ) by A3, A5;

hence c in S1 by A2; :: thesis: verum

( s in S1 iff ( s in C -States X & (s . a) . x <> f ) ) ) & ( for s being ManySortedFunction of X, the Sorts of C holds

( s in S2 iff ( s in C -States X & (s . a) . x <> f ) ) ) implies S1 = S2 )

assume that

A2: for s being ManySortedFunction of X, the Sorts of C holds

( s in S1 iff ( s in C -States X & (s . a) . x <> f ) ) and

A3: for s being ManySortedFunction of X, the Sorts of C holds

( s in S2 iff ( s in C -States X & (s . a) . x <> f ) ) ; :: thesis: S1 = S2

thus S1 c= S2 :: according to XBOOLE_0:def 10 :: thesis: S2 c= S1

proof

let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in S2 or c in S1 )
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in S1 or c in S2 )

assume A4: c in S1 ; :: thesis: c in S2

then reconsider s = c as ManySortedFunction of X, the Sorts of C by Th43;

( s in C -States X & (s . a) . x <> f ) by A2, A4;

hence c in S2 by A3; :: thesis: verum

end;assume A4: c in S1 ; :: thesis: c in S2

then reconsider s = c as ManySortedFunction of X, the Sorts of C by Th43;

( s in C -States X & (s . a) . x <> f ) by A2, A4;

hence c in S2 by A3; :: thesis: verum

assume A5: c in S2 ; :: thesis: c in S1

then reconsider s = c as ManySortedFunction of X, the Sorts of C by Th43;

( s in C -States X & (s . a) . x <> f ) by A3, A5;

hence c in S1 by A2; :: thesis: verum