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;
z in union A by A2, XBOOLE_0:def 4;
then consider X being set such that
A3: z in X and
A4: X in A by TARSKI:def 4;
A5: X misses B by A1, A4;
z in B by A2, XBOOLE_0:def 4;
then z in X /\ B by A3, XBOOLE_0:def 4;
hence contradiction by A5, XBOOLE_0:4; :: thesis: verum