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 A1, A2, ZFMISC_1:31;
then A4: B = A by ZFMISC_1:3;
{C} c= {A} by A1, A3, ZFMISC_1:31;
hence B = C by A4, ZFMISC_1:3; :: 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