let T be non empty TopSpace; :: thesis: for A being Subset of T
for F being Subset-Family of T st F = {A} holds
Der F = {(Der A)}
let A be Subset of T; :: thesis: for F being Subset-Family of T st F = {A} holds
Der F = {(Der A)}
let F be Subset-Family of T; :: thesis: ( F = {A} implies Der F = {(Der A)} )
assume A1: F = {A} ; :: thesis: Der F = {(Der A)}
thus Der F c= {(Der A)} :: according to XBOOLE_0:def 10 :: thesis: {(Der A)} c= Der F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Der F or x in {(Der A)} )
assume A2: x in Der F ; :: thesis: x in {(Der A)}
then reconsider B = x as Subset of T ;
consider C being Subset of T such that
A3: B = Der C and
A4: C in F by A2, Def6;
C = A by A1, A4, TARSKI:def 1;
hence x in {(Der A)} by A3, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Der A)} or x in Der F )
assume x in {(Der A)} ; :: thesis: x in Der F
then A5: x = Der A by TARSKI:def 1;
A in F by A1, TARSKI:def 1;
hence x in Der F by A5, Def6; :: thesis: verum