let I be set ; :: thesis: for X, Y being ManySortedSet of holds
( X /\ Y = [0] I iff X \ Y = X )
let X, Y be ManySortedSet of ; :: 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