let T be non empty TopSpace; :: thesis:
let F be Subset-Family of T; :: thesis:
assume ex A being Subset of T st F = {A} ; :: thesis:
then consider A being Subset of T such that
A1: F = {A} ;

let p be Point of T; :: thesis:
take O = [#] T; :: thesis:
thus p in O ; :: thesis:

let B, C be Subset of T; :: thesis:
assume that
A2: B in F and
A3: C in F ; :: thesis:
{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:

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:

end;

hence F is discrete ; :: thesis: