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