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

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

assume A1: X /\ Y = [[0]] I ; :: thesis: X \ Y = X
thus X \ Y = X \ (X /\ Y) by Th76
.= X by A1, Th65 ; :: thesis: verum

end;

thus ( X \ Y = X implies X /\ Y = [[0]] I ) by Th69; :: thesis: verum