let I be set ; :: thesis: for X, Y being ManySortedSet of I holds X \ Y = X \+\ (X /\ Y)
let X, Y be ManySortedSet of I; :: thesis: X \ Y = X \+\ (X /\ Y)
A1: X /\ Y c= X by Th15;
thus X \ Y = X \ (X /\ Y) by Th70
.= (X \ (X /\ Y)) \/ ([[0]] I) by Th22, Th43
.= X \+\ (X /\ Y) by A1, Th52 ; :: thesis: verum