let T be TopSpace; :: thesis: for A, B being Element of Closed_Domains_of T holds (CLD-Union T) . (A,B) = (D-Union T) . (A,B)
let A, B be Element of Closed_Domains_of T; :: thesis: (CLD-Union T) . (A,B) = (D-Union T) . (A,B)
A1: A in { D where D is Subset of T : D is closed_condensed } ;
Closed_Domains_of T c= Domains_of T by Th31;
then reconsider A0 = A, B0 = B as Element of Domains_of T ;
B in { E where E is Subset of T : E is closed_condensed } ;
then consider E being Subset of T such that
A2: E = B and
A3: E is closed_condensed ;
consider D being Subset of T such that
A4: D = A and
A5: D is closed_condensed by A1;
D \/ E is closed_condensed by A5, A3, TOPS_1:68;
then D \/ E is condensed by TOPS_1:66;
then A6: Int (Cl (A \/ B)) c= A \/ B by A4, A2, TOPS_1:def 6;
thus (CLD-Union T) . (A,B) = A \/ B by Def6
.= (Int (Cl (A0 \/ B0))) \/ (A0 \/ B0) by A6, XBOOLE_1:12
.= (D-Union T) . (A,B) by Def2 ; :: thesis: verum