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 /\ B) c= (union A) /\ (union B) by Th97;
(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 x in (union A) /\ (union B) ; :: thesis: x in union (A /\ B)
then A3: ( x in union A & x in union B ) 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;
consider Y being set such that
A6: x in Y and
A7: Y in B by A3, TARSKI:def 4;

now

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

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