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