let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is dense-in-itself holds
union F c= union (Der F)
let F be Subset-Family of T; :: thesis: ( F is dense-in-itself implies union F c= union (Der F) )
assume A1: F is dense-in-itself ; :: thesis: union F c= union (Der F)
thus union F c= union (Der F) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union F or x in union (Der F) )
assume x in union F ; :: thesis: x in union (Der F)
then consider A being set such that
A2: x in A and
A3: A in F by TARSKI:def 4;
reconsider A = A as Subset of T by A3;
A is dense-in-itself by A1, A3;
then A4: A c= Der A ;
Der A in Der F by A3, Def6;
hence x in union (Der F) by A2, A4, TARSKI:def 4; :: thesis: verum

end;