let T be non empty TopSpace; :: thesis: for F, G being Subset-Family of T st F c= G holds
Der F c= Der G
let F, G be Subset-Family of T; :: thesis: ( F c= G implies Der F c= Der G )
assume A1: F c= G ; :: thesis: Der F c= Der G
Der F c= Der G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Der F or x in Der G )
assume A2: x in Der F ; :: thesis: x in Der G
then reconsider A = x as Subset of T ;
ex B being Subset of T st
( A = Der B & B in F ) by A2, Def6;
hence x in Der G by A1, Def6; :: thesis: verum

end;

hence Der F c= Der G ; :: thesis: verum