let A, B be set ; :: thesis: union (A /\ B) c= (union A) /\ (union B)
let x be set ; :: 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 A & Y in B ) by A2, XBOOLE_0:def 4;
then ( x in union A & x in union B ) by A1, TARSKI:def 4;
hence x in (union A) /\ (union B) by XBOOLE_0:def 4; :: thesis: verum