let x be set ; :: thesis: for D being non empty set holds x /\ () = union { (x /\ d) where d is Element of D : verum }
let D be non empty set ; :: thesis: x /\ () = 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 /\ ()
let a be object ; :: thesis: ( a in x /\ () implies a in union { (x /\ d) where d is Element of D : verum } )
assume A1: a in x /\ () ; :: 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 ;
then a in x /\ Z by ;
hence a in union { (x /\ d) where d is Element of D : verum } by ; :: 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 /\ () )
assume a in union { (x /\ d) where d is Element of D : verum } ; :: thesis: a in x /\ ()
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 ;
then A8: a in union D by TARSKI:def 4;
a in x by ;
hence a in x /\ () by ; :: thesis: verum