let T be non empty TopSpace; :: thesis: for A, B being Subset of T holds (A \/ B) ^0 = (A ^0) \/ (B ^0)
let A, B be Subset of T; :: thesis: (A \/ B) ^0 = (A ^0) \/ (B ^0)
thus (A \/ B) ^0 c= (A ^0) \/ (B ^0) :: according to XBOOLE_0:def 10 :: thesis: (A ^0) \/ (B ^0) c= (A \/ B) ^0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A \/ B) ^0 or x in (A ^0) \/ (B ^0) )
assume A1: x in (A \/ B) ^0 ; :: thesis: x in (A ^0) \/ (B ^0)
then reconsider x9 = x as Point of T ;
x9 is_a_condensation_point_of A \/ B by A1, Def10;
then ( x9 is_a_condensation_point_of A or x9 is_a_condensation_point_of B ) by Th53;
then ( x9 in A ^0 or x9 in B ^0 ) by Def10;
hence x in (A ^0) \/ (B ^0) by XBOOLE_0:def 3; :: thesis: verum

end;

( A ^0 c= (A \/ B) ^0 & B ^0 c= (A \/ B) ^0 ) by Th52, XBOOLE_1:7;
hence (A ^0) \/ (B ^0) c= (A \/ B) ^0 by XBOOLE_1:8; :: thesis: verum