let A, B be set ; :: thesis: union (A /\ B) c= (union A) /\ (union B)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (A /\ B) or x in (union A) /\ (union B) )
assume x in union (A /\ B) ; :: thesis: x in (union A) /\ (union B)
then consider Y being set such that
A1: x in Y and
A2: Y in A /\ B by TARSKI:def 4;
Y in B by A2, XBOOLE_0:def 4;
then A3: x in union B by A1, TARSKI:def 4;
Y in A by A2, XBOOLE_0:def 4;
then x in union A by A1, TARSKI:def 4;
hence x in (union A) /\ (union B) by A3, XBOOLE_0:def 4; :: thesis: verum