let T be TopSpace; 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; (OPD-Union T) . (A,B) = (D-Union T) . (A,B)
A in { D where D is Subset of T : D is open_condensed }
;
then consider D being Subset of T such that
A1:
D = A
and
A2:
D is open_condensed
;
A3:
A \/ B c= Cl (A \/ B)
by PRE_TOPC:18;
Open_Domains_of T c= Domains_of T
by Th35;
then reconsider A0 = A, B0 = B as Element of Domains_of T ;
B in { E where E is Subset of T : E is open_condensed }
;
then consider E being Subset of T such that
A4:
E = B
and
A5:
E is open_condensed
;
A6:
E is open
by A5, TOPS_1:67;
D is open
by A2, TOPS_1:67;
then A7:
Int (D \/ E) = D \/ E
by A6, TOPS_1:23;
thus (OPD-Union T) . (A,B) =
Int (Cl (A \/ B))
by Def10
.=
(Int (Cl (A0 \/ B0))) \/ (A0 \/ B0)
by A1, A4, A7, A3, TOPS_1:19, XBOOLE_1:12
.=
(D-Union T) . (A,B)
by Def2
; verum