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