let T be TopSpace; :: thesis: 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; :: thesis: (OPD-Meet T) . A,B = (D-Meet 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 /\ E is open_condensed by A2, A3, TOPS_1:109;
then A /\ B is condensed by A2, A3, TOPS_1:107;
then A4: A /\ B c= Cl (Int (A /\ B)) by TOPS_1:def 6;
reconsider A0 = A, B0 = B as Element of Domains_of T ;
thus (OPD-Meet T) . A,B = A /\ B by Def11
.= (Cl (Int (A0 /\ B0))) /\ (A0 /\ B0) by A4, XBOOLE_1:28
.= (D-Meet T) . A,B by Def3 ; :: thesis: verum