:: deftheorem Def1 defines Fr TOPGEN_1:def 1 :
for T being TopSpace
for F, b₃ being Subset-Family of T holds
( b₃ = Fr F iff for A being Subset of T holds
( A in b₃ iff ex B being Subset of T st
( A = Fr B & B in F ) ) );