let A, B, C be set ; :: thesis: A \+\ C = (A \+\ B) \+\ (B \+\ C)
(A \+\ B) \+\ B = A \+\ (B \+\ B) by XBOOLE_1:91
.= A \+\ {} by XBOOLE_1:92
.= A ;
hence A \+\ C = (A \+\ B) \+\ (B \+\ C) by XBOOLE_1:91; :: thesis: verum