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

proof

let e be object ; :: 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 X ; :: thesis: verum