:: deftheorem Def2 defines clf PCOMPS_1:def 2 :
for T being TopStruct
for FX, b₃ being Subset-Family of T holds
( b₃ = clf FX iff for Z being Subset of T holds
( Z in b₃ iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) );