let T be non empty TopSpace; :: thesis: for F, G being Subset-Family of T holds Der (F \/ G) = (Der F) \/ (Der G)
let F, G be Subset-Family of T; :: thesis: Der (F \/ G) = (Der F) \/ (Der G)
thus Der (F \/ G) c= (Der F) \/ (Der G) :: according to XBOOLE_0:def 10 :: thesis: (Der F) \/ (Der G) c= Der (F \/ G)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Der (F \/ G) or x in (Der F) \/ (Der G) )
assume A1: x in Der (F \/ G) ; :: thesis: x in (Der F) \/ (Der G)
then reconsider A = x as Subset of T ;
consider B being Subset of T such that
A2: A = Der B and
A3: B in F \/ G by A1, Def6;
per cases ( B in F or B in G ) by A3, XBOOLE_0:def 3;
end;
end;
( Der F c= Der (F \/ G) & Der G c= Der (F \/ G) ) by Th26, XBOOLE_1:7;
hence (Der F) \/ (Der G) c= Der (F \/ G) by XBOOLE_1:8; :: thesis: verum