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} ;

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 ) )

hence
F is discrete
; :: thesis: verum( 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

B = C ; :: thesis: verum

end;( 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

hence
for B, C being Subset of T st B in F & C in F & O meets B & O meets C 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;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

B = C ; :: thesis: verum