defpred S1[ set , set ] means for A, B being Element of Closed_Domains_of T st $1 = [A,B] holds
$2 = Cl (Int (A /\ B));
set D = [:(Closed_Domains_of T),(Closed_Domains_of T):];
A1:
for a being Element of [:(Closed_Domains_of T),(Closed_Domains_of T):] ex b being Element of Closed_Domains_of T st S1[a,b]
proof
let a be
Element of
[:(Closed_Domains_of T),(Closed_Domains_of T):];
ex b being Element of Closed_Domains_of T st S1[a,b]
reconsider G =
a `1 ,
F =
a `2 as
Element of
Closed_Domains_of T ;
Cl (Int (G /\ F)) is
closed_condensed
by Th22;
then
Cl (Int (G /\ F)) in { E where E is Subset of T : E is closed_condensed }
;
then reconsider b =
Cl (Int (G /\ F)) as
Element of
Closed_Domains_of T ;
take
b
;
S1[a,b]
let A,
B be
Element of
Closed_Domains_of T;
( a = [A,B] implies b = Cl (Int (A /\ B)) )
assume
a = [A,B]
;
b = Cl (Int (A /\ B))
then A2:
[A,B] = [G,F]
by MCART_1:21;
then
A = G
by XTUPLE_0:1;
hence
b = Cl (Int (A /\ B))
by A2, XTUPLE_0:1;
verum
end;
consider h being Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Closed_Domains_of T) such that
A3:
for a being Element of [:(Closed_Domains_of T),(Closed_Domains_of T):] holds S1[a,h . a]
from FUNCT_2:sch 3(A1);
take
h
; for A, B being Element of Closed_Domains_of T holds h . (A,B) = Cl (Int (A /\ B))
let A, B be Element of Closed_Domains_of T; h . (A,B) = Cl (Int (A /\ B))
thus h . (A,B) =
h . [A,B]
.=
Cl (Int (A /\ B))
by A3
; verum