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