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

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

hence
union A is Subset of X
; :: thesis: verum
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;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