let T be non empty TopSpace; :: thesis: for A, B being Subset of T holds Der (A \/ B) = (Der A) \/ (Der B)
let A, B be Subset of T; :: thesis: Der (A \/ B) = (Der A) \/ (Der B)
thus Der (A \/ B) c= (Der A) \/ (Der B) :: according to XBOOLE_0:def 10 :: thesis: (Der A) \/ (Der B) c= Der (A \/ B)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Der (A \/ B) or x in (Der A) \/ (Der B) )
assume x in Der (A \/ B) ; :: thesis: x in (Der A) \/ (Der B)
then x is_an_accumulation_point_of A \/ B by Th16;
then A1: x in Cl ((A \/ B) \ {x}) ;
(A \/ B) \ {x} = (A \ {x}) \/ (B \ {x}) by XBOOLE_1:42;
then Cl ((A \/ B) \ {x}) = (Cl (A \ {x})) \/ (Cl (B \ {x})) by PRE_TOPC:20;
then ( x in Cl (A \ {x}) or x in Cl (B \ {x}) ) by A1, XBOOLE_0:def 3;
then ( x is_an_accumulation_point_of A or x is_an_accumulation_point_of B ) ;
then ( x in Der A or x in Der B ) by Th16;
hence x in (Der A) \/ (Der B) by XBOOLE_0:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Der A) \/ (Der B) or x in Der (A \/ B) )
assume x in (Der A) \/ (Der B) ; :: thesis: x in Der (A \/ B)
then ( x in Der A or x in Der B ) by XBOOLE_0:def 3;
then A2: ( x is_an_accumulation_point_of A or x is_an_accumulation_point_of B ) by Th16;
x in Cl ((A \/ B) \ {x})
proof
B \ {x} c= (A \/ B) \ {x} by XBOOLE_1:7, XBOOLE_1:33;
then A3: Cl (B \ {x}) c= Cl ((A \/ B) \ {x}) by PRE_TOPC:19;
A \ {x} c= (A \/ B) \ {x} by XBOOLE_1:7, XBOOLE_1:33;
then A4: Cl (A \ {x}) c= Cl ((A \/ B) \ {x}) by PRE_TOPC:19;
per cases ( x in Cl (A \ {x}) or x in Cl (B \ {x}) ) by A2;
suppose x in Cl (A \ {x}) ; :: thesis: x in Cl ((A \/ B) \ {x})
hence x in Cl ((A \/ B) \ {x}) by A4; :: thesis: verum
end;
suppose x in Cl (B \ {x}) ; :: thesis: x in Cl ((A \/ B) \ {x})
hence x in Cl ((A \/ B) \ {x}) by A3; :: thesis: verum
end;
end;
end;
then x is_an_accumulation_point_of A \/ B ;
hence x in Der (A \/ B) by Th16; :: thesis: verum