let A, B be set ; :: thesis: ( ( for X being set st X in A holds
X misses B ) implies union A misses B )
assume A1: for X being set st X in A holds
X misses B ; :: thesis: union A misses B
assume union A meets B ; :: thesis: contradiction
then consider z being set such that
A2: z in (union A) /\ B by XBOOLE_0:4;
A3: ( z in union A & z in B ) by A2, XBOOLE_0:def 4;
then consider X being set such that
A4: z in X and
A5: X in A by TARSKI:def 4;
( z in X /\ B & X misses B ) by A1, A3, A4, A5, XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:4; :: thesis: verum