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