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 set ; :: 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 x' = x as Point of T ;
x' is_a_condensation_point_of A \/ B by A1, Def10;
then ( x' is_a_condensation_point_of A or x' is_a_condensation_point_of B ) by Th56;
then ( x' in A ^0 or x' in B ^0 ) by Def10;
hence x in (A ^0 ) \/ (B ^0 ) by XBOOLE_0:def 3; :: thesis: verum

end;

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