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

hereby :: thesis: ( X c= Y implies X \ Y = [[0]] I )

assume A1: X \ Y = [[0]] I ; :: thesis: X c= Y

now

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

end;

hence X c= Y by Def5; :: thesis: verum

end;

assume A2: X c= Y ; :: thesis: X \ Y = [[0]] I

now

let i be set ; :: thesis: ( i in I implies (X \ Y) . i = {} )
assume A3: i in I ; :: thesis: (X \ Y) . i = {}
then A4: X . i c= Y . i by A2, Def5;
thus (X \ Y) . i = (X . i) \ (Y . i) by A3, Def9
.= {} by A4, XBOOLE_1:37 ; :: thesis: verum

end;

hence X \ Y = [[0]] I by Th6; :: thesis: verum