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 object 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;
z in B by A2, XBOOLE_0:def 4;
then z in X /\ B by A3, XBOOLE_0:def 4;
hence contradiction by A1, A4, XBOOLE_0:4; :: thesis: verum