let X, Y be set ; :: thesis: X \ Y = X \+\ (X /\ Y)
X /\ Y c= X by Th17;
then (X /\ Y) \ X = {} by Lm1;
hence X \ Y = X \+\ (X /\ Y) by Th47; :: thesis: verum