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 Th56;
thus X /\ Y = X \ (X \ Y) by Th68
.= (X \ (X \ Y)) \/ ([[0]] I) by Th22, Th43
.= X \+\ (X \ Y) by A1, Th52 ; :: thesis: verum