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 }

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

A5: a in Z and

A6: Z in { (x /\ d) where d is Element of D : verum } by TARSKI:def 4;

consider d being Element of D such that

A7: Z = x /\ d and

verum by A6;

a in d by A5, A7, XBOOLE_0:def 4;

then A8: a in union D by TARSKI:def 4;

a in x by A5, A7, XBOOLE_0:def 4;

hence a in x /\ (union D) by A8, XBOOLE_0:def 4; :: thesis: 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 object ; :: 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) )let a be object ; :: thesis: ( a in x /\ (union D) implies a in union { (x /\ d) where d is Element of D : verum } )

assume A1: a in x /\ (union D) ; :: thesis: a in union { (x /\ d) where d is Element of D : verum }

then a in union D by XBOOLE_0:def 4;

then consider Z being set such that

A2: a in Z and

A3: Z in D by TARSKI:def 4;

A4: x /\ Z in { (x /\ d) where d is Element of D : verum } by A3;

a in x by A1, XBOOLE_0:def 4;

then a in x /\ Z by A2, XBOOLE_0:def 4;

hence a in union { (x /\ d) where d is Element of D : verum } by A4, TARSKI:def 4; :: thesis: verum

end;assume A1: a in x /\ (union D) ; :: thesis: a in union { (x /\ d) where d is Element of D : verum }

then a in union D by XBOOLE_0:def 4;

then consider Z being set such that

A2: a in Z and

A3: Z in D by TARSKI:def 4;

A4: x /\ Z in { (x /\ d) where d is Element of D : verum } by A3;

a in x by A1, XBOOLE_0:def 4;

then a in x /\ Z by A2, XBOOLE_0:def 4;

hence a in union { (x /\ d) where d is Element of D : verum } by A4, TARSKI:def 4; :: thesis: verum

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

A5: a in Z and

A6: Z in { (x /\ d) where d is Element of D : verum } by TARSKI:def 4;

consider d being Element of D such that

A7: Z = x /\ d and

verum by A6;

a in d by A5, A7, XBOOLE_0:def 4;

then A8: a in union D by TARSKI:def 4;

a in x by A5, A7, XBOOLE_0:def 4;

hence a in x /\ (union D) by A8, XBOOLE_0:def 4; :: thesis: verum