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