let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F = {} holds
Der F = {}
let F be Subset-Family of T; :: thesis: ( F = {} implies Der F = {} )
assume A1: F = {} ; :: thesis: Der F = {}
assume Der F <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in Der F by XBOOLE_0:def 1;
ex B being Subset of T st
( x = Der B & B in F ) by A2, Def6;
hence contradiction by A1; :: thesis: verum