let I be set ; :: thesis: for X, Y being ManySortedSet of I holds X /\ Y = (X \+\ Y) \+\ (X \/ Y)
let X, Y be ManySortedSet of I; :: thesis: X /\ Y = (X \+\ Y) \+\ (X \/ Y)
thus X /\ Y = X \+\ (X \ Y) by Th101
.= X \+\ (Y \+\ (X \/ Y)) by Th103
.= (X \+\ Y) \+\ (X \/ Y) by Th98 ; :: thesis: verum