let x be set ; :: thesis: for D being non empty set holds x /\ (union D) = union { (x /\ d) where d is Element of D : verum }
let D be non empty set ; :: thesis: x /\ (union D) = union { (x /\ d) where d is Element of D : verum }

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union { (x /\ d) where d is Element of D : verum } c= x /\ (union D)

let a be set ; :: thesis: ( a in x /\ (union D) implies a in union { (x /\ d) where d is Element of D : verum } )
assume a in x /\ (union D) ; :: thesis: a in union { (x /\ d) where d is Element of D : verum }
then A1: ( a in x & a in union D ) by XBOOLE_0:def 4;
then consider Z being set such that
A2: ( a in Z & Z in D ) by TARSKI:def 4;
A3: a in x /\ Z by A1, A2, XBOOLE_0:def 4;
x /\ Z in { (x /\ d) where d is Element of D : verum } by A2;
hence a in union { (x /\ d) where d is Element of D : verum } by A3, TARSKI:def 4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (x /\ d) where d is Element of D : verum } or a in x /\ (union D) )
assume a in union { (x /\ d) where d is Element of D : verum } ; :: thesis: a in x /\ (union D)
then consider Z being set such that
A4: ( a in Z & Z in { (x /\ d) where d is Element of D : verum } ) by TARSKI:def 4;
consider d being Element of D such that
A5: Z = x /\ d and
verum by A4;
A6: ( a in x & a in d ) by A4, A5, XBOOLE_0:def 4;
then a in union D by TARSKI:def 4;
hence a in x /\ (union D) by A6, XBOOLE_0:def 4; :: thesis: verum