defpred S₁[ 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 S₁[a,b]

proof

let a be Element of [:(Open_Domains_of T),(Open_Domains_of T):]; :: thesis: ex b being Element of Open_Domains_of T st S₁[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 ; :: thesis: S₁[a,b]
let A, B be Element of Open_Domains_of T; :: thesis: ( a = [A,B] implies b = Int (Cl (A \/ B)) )
assume a = [A,B] ; :: thesis: 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; :: thesis: 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 S₁[a,h . a] from FUNCT_2:sch 3(A1);
take h ; :: thesis: 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; :: thesis: h . (A,B) = Int (Cl (A \/ B))
thus h . (A,B) = h . [A,B]
.= Int (Cl (A \/ B)) by A3 ; :: thesis: verum