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