let T be TopSpace; for A, B being Element of Open_Domains_of T holds (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B)
let A, B be Element of Open_Domains_of T; (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B)
A1:
A in { D where D is Subset of T : D is open_condensed }
;
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
A2:
E = B
and
A3:
E is open_condensed
;
consider D being Subset of T such that
A4:
D = A
and
A5:
D is open_condensed
by A1;
D /\ E is open_condensed
by A5, A3, TOPS_1:69;
then
A /\ B is condensed
by A4, A2, TOPS_1:67;
then A6:
A /\ B c= Cl (Int (A /\ B))
by TOPS_1:def 6;
thus (OPD-Meet T) . (A,B) =
A /\ B
by Def11
.=
(Cl (Int (A0 /\ B0))) /\ (A0 /\ B0)
by A6, XBOOLE_1:28
.=
(D-Meet T) . (A,B)
by Def3
; verum