let I be set ; :: thesis: for X, Y being ManySortedSet of I st X c= Y \ X holds
X = [[0]] I
let X, Y be ManySortedSet of I; :: thesis: ( X c= Y \ X implies X = [[0]] I )
assume A1: X c= Y \ X ; :: thesis: X = [[0]] I

now

let i be set ; :: thesis: ( i in I implies X . i = ([[0]] I) . i )
assume A2: i in I ; :: thesis: X . i = ([[0]] I) . i
then X . i c= (Y \ X) . i by A1, Def5;
then X . i c= (Y . i) \ (X . i) by A2, Def9;
hence X . i = {} by XBOOLE_1:38
.= ([[0]] I) . i by Th5 ;
:: thesis: verum

end;

hence X = [[0]] I by Th3; :: thesis: verum