let T be TopSpace; :: thesis: for A, B being Element of Closed_Domains_of T holds (CLD-Meet T) . A,B = (D-Meet T) . A,B
let A, B be Element of Closed_Domains_of T; :: thesis: (CLD-Meet T) . A,B = (D-Meet T) . A,B
A1: ( A in { D where D is Subset of T : D is closed_condensed } & B in { E where E is Subset of T : E is closed_condensed } ) ;
then consider D being Subset of T such that
A2: ( D = A & D is closed_condensed ) ;
consider E being Subset of T such that
A3: ( E = B & E is closed_condensed ) by A1;
( D is closed & E is closed ) by A2, A3, TOPS_1:106;
then D /\ E is closed by TOPS_1:35;
then A4: Cl (D /\ E) = D /\ E by PRE_TOPC:52;
A5: Int (A /\ B) c= A /\ B by TOPS_1:44;
reconsider A0 = A, B0 = B as Element of Domains_of T ;
thus (CLD-Meet T) . A,B = Cl (Int (A /\ B)) by Def7
.= (Cl (Int (A0 /\ B0))) /\ (A0 /\ B0) by A2, A3, A4, A5, PRE_TOPC:49, XBOOLE_1:28
.= (D-Meet T) . A,B by Def3 ; :: thesis: verum