let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st ex A being Subset of T st F = {A} holds
F is discrete

let F be Subset-Family of T; :: thesis: ( ex A being Subset of T st F = {A} implies F is discrete )
assume ex A being Subset of T st F = {A} ; :: thesis: F is discrete
then consider A being Subset of T such that
A1: F = {A} ;
now :: thesis: for p being Point of T ex O being Element of bool the carrier of T st
( p in O & ( for B, C being Subset of T st B in F & C in F & O meets B & O meets C holds
B = C ) )
let p be Point of T; :: thesis: ex O being Element of bool the carrier of T st
( p in O & ( for B, C being Subset of T st B in F & C in F & O meets B & O meets C holds
B = C ) )

take O = [#] T; :: thesis: ( p in O & ( for B, C being Subset of T st B in F & C in F & O meets B & O meets C holds
B = C ) )

thus p in O ; :: thesis: for B, C being Subset of T st B in F & C in F & O meets B & O meets C holds
B = C

now :: thesis: for B, C being Subset of T st B in F & C in F holds
B = C
let B, C be Subset of T; :: thesis: ( B in F & C in F implies B = C )
assume that
A2: B in F and
A3: C in F ; :: thesis: B = C
{B} c= {A} by ;
then A4: B = A by ZFMISC_1:3;
{C} c= {A} by ;
hence B = C by ; :: thesis: verum
end;
hence for B, C being Subset of T st B in F & C in F & O meets B & O meets C holds
B = C ; :: thesis: verum
end;
hence F is discrete ; :: thesis: verum