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 Th70;

assume C misses D ; :: thesis: (A \/ B) \/ C misses D

hence (A \/ B) \/ C misses D by A1, Th70; :: thesis: verum

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 Th70;

assume C misses D ; :: thesis: (A \/ B) \/ C misses D

hence (A \/ B) \/ C misses D by A1, Th70; :: thesis: verum