let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds union (Der F) c= Der (union F)
let F be Subset-Family of T; :: thesis: union (Der F) c= Der (union F)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (Der F) or x in Der (union F) )
assume x in union (Der F) ; :: thesis: x in Der (union F)
then consider Y being set such that
A1: x in Y and
A2: Y in Der F by TARSKI:def 4;
reconsider Y = Y as Subset of T by A2;
consider B being Subset of T such that
A3: Y = Der B and
A4: B in F by A2, Def6;
Der B c= Der (union F) by A4, Th30, ZFMISC_1:74;
hence x in Der (union F) by A1, A3; :: thesis: verum