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