let I be set ; :: thesis: for Y, Z being ManySortedSet of I
for X being V8() ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff ( x in Y & x in Z ) ) ) holds
X = Y /\ Z
let Y, Z be ManySortedSet of I; :: thesis: for X being V8() ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff ( x in Y & x in Z ) ) ) holds
X = Y /\ Z
let X be V8() ManySortedSet of I; :: thesis: ( ( for x being ManySortedSet of I holds
( x in X iff ( x in Y & x in Z ) ) ) implies X = Y /\ Z )
assume A1: for x being ManySortedSet of I holds
( x in X iff ( x in Y & x in Z ) ) ; :: thesis: X = Y /\ Z

now

let x be ManySortedSet of I; :: thesis: ( ( x in X implies x in Y /\ Z ) & ( x in Y /\ Z implies x in X ) )

hereby :: thesis: ( x in Y /\ Z implies x in X )

assume x in X ; :: thesis: x in Y /\ Z
then ( x in Y & x in Z ) by A1;
hence x in Y /\ Z by Th8; :: thesis: verum

end;

assume x in Y /\ Z ; :: thesis: x in X
then ( x in Y & x in Z ) by Th8;
hence x in X by A1; :: thesis: verum

end;

hence X = Y /\ Z by Th147; :: thesis: verum