let T be non empty TopSpace; :: thesis: for A, B being Subset of T st A c= B holds
Der A c= Der B
let A, B be Subset of T; :: thesis: ( A c= B implies Der A c= Der B )
assume A1: A c= B ; :: thesis: Der A c= Der B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Der A or x in Der B )
assume A2: x in Der A ; :: thesis: x in Der B
then reconsider x9 = x as Point of T ;
for U being open Subset of T st x9 in U holds
ex y being Point of T st
( y in B /\ U & x9 <> y )

proof

let U be open Subset of T; :: thesis: ( x9 in U implies ex y being Point of T st
( y in B /\ U & x9 <> y ) )
assume x9 in U ; :: thesis: ex y being Point of T st
( y in B /\ U & x9 <> y )
then A3: ex y being Point of T st
( y in A /\ U & x9 <> y ) by A2, Th17;
A /\ U c= B /\ U by A1, XBOOLE_1:26;
hence ex y being Point of T st
( y in B /\ U & x9 <> y ) by A3; :: thesis: verum

end;

hence x in Der B by Th17; :: thesis: verum