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

now

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

proof

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, Def1;
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;

hence 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: verum

end;

hence F is discrete by Def1; :: thesis: verum