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 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;
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) )
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