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 = {} )
reconsider CFX = clf FX as set ;
set X = the Element of CFX;
assume A1: FX = {} ; :: thesis: clf FX = {}
A2: for X being set holds not X in CFX
proof
let X be set ; :: thesis: not X in CFX
assume A3: 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 A3, Def2;
hence contradiction by A1; :: thesis: verum
end;
assume not clf FX = {} ; :: thesis: contradiction
then the Element of CFX in CFX ;
hence contradiction by A2; :: thesis: verum