let T be TopSpace; :: thesis: for FX being Subset-Family of T st FX = {} holds
clf FX = {}
let FX be Subset-Family of T; :: thesis: ( FX = {} implies clf FX = {} )
assume A1: FX = {} ; :: thesis: clf FX = {}
reconsider CFX = clf FX as set ;
assume A2: not clf FX = {} ; :: thesis: contradiction
A3: for X being set holds not X in CFX

proof

let X be set ; :: thesis: not X in CFX
assume A4: X in CFX ; :: thesis: contradiction
then reconsider X = X as Subset of T ;
ex V being Subset of T st
( X = Cl V & V in FX ) by A4, Def3;
hence contradiction by A1; :: thesis: verum

end;

consider X being Element of CFX;
X in CFX by A2;
hence contradiction by A3; :: thesis: verum