let T be TopSpace; 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; (CLD-Meet T) . (A,B) = (D-Meet T) . (A,B)
A in { D where D is Subset of T : D is closed_condensed }
;
then consider D being Subset of T such that
A1:
D = A
and
A2:
D is closed_condensed
;
A3:
Int (A /\ B) c= A /\ B
by TOPS_1:16;
Closed_Domains_of T c= Domains_of T
by Th31;
then reconsider A0 = A, B0 = B as Element of Domains_of T ;
B in { E where E is Subset of T : E is closed_condensed }
;
then consider E being Subset of T such that
A4:
E = B
and
A5:
E is closed_condensed
;
A6:
E is closed
by A5, TOPS_1:66;
D is closed
by A2, TOPS_1:66;
then A7:
Cl (D /\ E) = D /\ E
by A6, PRE_TOPC:22;
thus (CLD-Meet T) . (A,B) =
Cl (Int (A /\ B))
by Def7
.=
(Cl (Int (A0 /\ B0))) /\ (A0 /\ B0)
by A1, A4, A7, A3, PRE_TOPC:19, XBOOLE_1:28
.=
(D-Meet T) . (A,B)
by Def3
; verum