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 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 consider u being set such that
A1: ( e in u & u in A ) by TARSKI:def 4;
e in union D by A1, TARSKI:def 4;
hence e in X ; :: thesis: verum

end;

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