let X, Y be set ; :: thesis: X \/ (X \/ Y) = X \/ Y
X \/ (X \/ Y) = (X \/ X) \/ Y by Th4
.= X \/ Y ;
hence X \/ (X \/ Y) = X \/ Y ; :: thesis: verum