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 Th93
.= X \+\ (Y \+\ (X \/ Y)) by Th95
.= (X \+\ Y) \+\ (X \/ Y) by Th90 ; :: thesis: verum