let X be non empty set ; :: thesis: for D being Subset-Family of
for A being Subset of holds union A is Subset of
let D be Subset-Family of ; :: thesis: for A being Subset of holds union A is Subset of
let A be Subset of ; :: thesis: union A is Subset of
union A c= X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in union A or e in X )
assume e in union A ; :: thesis: e in X
then ex u being set st
( e in u & u in A ) by TARSKI:def 4;
then e in union D by TARSKI:def 4;
hence e in X ; :: thesis: verum

end;

hence union A is Subset of ; :: thesis: verum