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

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

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

( A ^0 c= (A \/ B) ^0 & B ^0 c= (A \/ B) ^0 )
by Th52, XBOOLE_1:7;
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;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

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