let T be TopSpace; :: thesis: for A, B being Element of Open_Domains_of T holds (OPD-Union T) . A,B = (D-Union T) . A,B
let A, B be Element of Open_Domains_of T; :: thesis: (OPD-Union T) . A,B = (D-Union T) . A,B
A1: ( A in { D where D is Subset of T : D is open_condensed } & B in { E where E is Subset of T : E is open_condensed } ) ;
then consider D being Subset of T such that
A2: ( D = A & D is open_condensed ) ;
consider E being Subset of T such that
A3: ( E = B & E is open_condensed ) by A1;
( D is open & E is open ) by A2, A3, TOPS_1:107;
then D \/ E is open by TOPS_1:37;
then A4: Int (D \/ E) = D \/ E by TOPS_1:55;
A5: A \/ B c= Cl (A \/ B) by PRE_TOPC:48;
reconsider A0 = A, B0 = B as Element of Domains_of T ;
thus (OPD-Union T) . A,B = Int (Cl (A \/ B)) by Def10
.= (Int (Cl (A0 \/ B0))) \/ (A0 \/ B0) by A2, A3, A4, A5, TOPS_1:48, XBOOLE_1:12
.= (D-Union T) . A,B by Def2 ; :: thesis: verum