let A, B, C, D, Z be set ; :: thesis: ( A misses Z & B misses Z & C misses Z & D misses Z implies ((A \/ B) \/ C) \/ D misses Z )
assume ( A misses Z & B misses Z & C misses Z ) ; :: thesis: ( not D misses Z or ((A \/ B) \/ C) \/ D misses Z )
then (A \/ B) \/ C misses Z by XBOOLE_1:114;
hence ( not D misses Z or ((A \/ B) \/ C) \/ D misses Z ) by XBOOLE_1:70; :: thesis: verum