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 :: 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 ) ) )
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;
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 ; :: thesis: verum