let T be TopSpace; :: thesis: for F being Subset-Family of T holds
( F = {} iff Cl F = {} )
let F be Subset-Family of T; :: thesis: ( F = {} iff Cl F = {} )
thus ( F = {} implies Cl F = {} ) by PCOMPS_1:12; :: thesis: ( Cl F = {} implies F = {} )
assume A1: Cl F = {} ; :: thesis: F = {}
set B = the Element of F;
assume A2: F <> {} ; :: thesis: contradiction
then reconsider B = the Element of F as Subset of T by TARSKI:def 3;
Cl B in Cl F by A2, PCOMPS_1:def 2;
hence contradiction by A1; :: thesis: verum