let A, B, C, Z be set ; :: thesis: ( A c= Z & B c= Z & C c= Z implies (A \/ B) \/ C c= Z )
assume ( A c= Z & B c= Z ) ; :: thesis: ( not C c= Z or (A \/ B) \/ C c= Z )
then A \/ B c= Z by XBOOLE_1:8;
hence ( not C c= Z or (A \/ B) \/ C c= Z ) by XBOOLE_1:8; :: thesis: verum