let A, B be set ; :: thesis: ( ( for X, Y being set st X <> Y & X in A \/ B & Y in A \/ B holds
X misses Y ) implies union (A /\ B) = (union A) /\ (union B) )
assume A1: for X, Y being set st X <> Y & X in A \/ B & Y in A \/ B holds
X misses Y ; :: thesis: union (A /\ B) = (union A) /\ (union B)
A2: (union A) /\ (union B) c= union (A /\ B)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (union A) /\ (union B) or x in union (A /\ B) )
assume A3: x in (union A) /\ (union B) ; :: thesis: x in union (A /\ B)
then x in union A by XBOOLE_0:def 4;
then consider X being set such that
A4: x in X and
A5: X in A by TARSKI:def 4;
x in union B by A3, XBOOLE_0:def 4;
then consider Y being set such that
A6: x in Y and
A7: Y in B by TARSKI:def 4;

now

x in X /\ Y by A4, A6, XBOOLE_0:def 4;
then A8: X meets Y by XBOOLE_0:4;
assume A9: X <> Y ; :: thesis: contradiction
( X in A \/ B & Y in A \/ B ) by A5, A7, XBOOLE_0:def 3;
hence contradiction by A1, A9, A8; :: thesis: verum

end;

then Y in A /\ B by A5, A7, XBOOLE_0:def 4;
hence x in union (A /\ B) by A6, TARSKI:def 4; :: thesis: verum

end;

union (A /\ B) c= (union A) /\ (union B) by Th97;
hence union (A /\ B) = (union A) /\ (union B) by A2, XBOOLE_0:def 10; :: thesis: verum