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)
(union A) /\ (union B) c= union (A /\ B)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union A) /\ (union B) or x in union (A /\ B) )
assume A2: 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
A3: x in X and
A4: X in A by TARSKI:def 4;
x in union B by A2, XBOOLE_0:def 4;
then consider Y being set such that
A5: x in Y and
A6: Y in B by TARSKI:def 4;
now :: thesis: not X <> Y
A7: x in X /\ Y by A3, A5, XBOOLE_0:def 4;
assume A8: X <> Y ; :: thesis: contradiction
( X in A \/ B & Y in A \/ B ) by A4, A6, XBOOLE_0:def 3;
hence contradiction by A1, A8, A7, XBOOLE_0:4; :: thesis: verum
end;
then Y in A /\ B by A4, A6, XBOOLE_0:def 4;
hence x in union (A /\ B) by A5, TARSKI:def 4; :: thesis: verum
end;
hence union (A /\ B) = (union A) /\ (union B) by Th78; :: thesis: verum