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

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

let B, C be Subset of T; :: thesis: ( B in F & C in F implies B = C )
assume ( B in F & C in F ) ; :: thesis: B = C
then ( {B} c= {A} & {C} c= {A} ) by A1, ZFMISC_1:37;
then ( B = A & C = A ) by ZFMISC_1:6;
hence B = C ; :: 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 by Def1; :: thesis: verum