let X, Y be set ; :: thesis: X /\ Y = (X \+\ Y) \+\ (X \/ Y)
X \+\ Y = (X \/ Y) \ (X /\ Y) by Lm5;
then X \+\ Y c= X \/ Y by Th36;
then A1: (X \+\ Y) \ (X \/ Y) = {} by Lm1;
X \/ Y = (X \+\ Y) \/ (X /\ Y) by Th93;
hence X /\ Y = (X \+\ Y) \+\ (X \/ Y) by A1, Lm4, Th88; :: thesis: verum