let X, Y be set ; :: thesis: X \+\ Y c= X \/ Y
X \+\ Y = (X \/ Y) \ (X /\ Y) by XBOOLE_1:101;
hence X \+\ Y c= X \/ Y ; :: thesis: verum