let I be set ; :: thesis: for Y, Z being ManySortedSet of I
for X being non-empty 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 non-empty 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 non-empty 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 :: thesis: for x being ManySortedSet of I holds
( ( x in X implies x in Y (/\) Z ) & ( x in Y (/\) Z implies x in X ) )

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 Th135; :: thesis: verum