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 Th17;
thus X \ Y = X \ (X /\ Y) by Th76
.= (X \ (X /\ Y)) \/ ([[0]] I) by Th53
.= X \+\ (X /\ Y) by A1, Th58 ; :: thesis: verum