let T be non empty TopSpace; :: thesis: for F, G being Subset-Family of T st F c= G & G is discrete holds

F is discrete

let F, G be Subset-Family of T; :: thesis: ( F c= G & G is discrete implies F is discrete )

assume that

A1: F c= G and

A2: G is discrete ; :: thesis: F is discrete

F is discrete

let F, G be Subset-Family of T; :: thesis: ( F c= G & G is discrete implies F is discrete )

assume that

A1: F c= G and

A2: G is discrete ; :: thesis: F is discrete

now :: thesis: for p being Point of T holds

( ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) & ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) )

hence
F is discrete
; :: thesis: verum( ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) & ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) )

let p be Point of T; :: thesis: ( ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) & ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) )

thus ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) :: thesis: ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) )

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) ; :: thesis: verum

end;( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) & ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) )

thus ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) :: thesis: ex O being open Subset of T st

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) )

proof

hence
ex O being open Subset of T st
consider U being open Subset of T such that

A3: ( p in U & ( for C, D being Subset of T st C in G & D in G & U meets C & U meets D holds

C = D ) ) by A2;

take O = U; :: thesis: ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) )

thus ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) by A1, A3; :: thesis: verum

end;A3: ( p in U & ( for C, D being Subset of T st C in G & D in G & U meets C & U meets D holds

C = D ) ) by A2;

take O = U; :: thesis: ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) )

thus ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) by A1, A3; :: thesis: verum

( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D ) ) ; :: thesis: verum