defpred S₁[ set , set ] means for A, B being Element of Domains_of T st $1 = [A,B] holds
$2 = (Cl (Int (A /\ B))) /\ (A /\ B);
set D = [:(Domains_of T),(Domains_of T):];
A1: for a being Element of [:(Domains_of T),(Domains_of T):] ex b being Element of Domains_of T st S₁[a,b]

proof

let a be Element of [:(Domains_of T),(Domains_of T):]; :: thesis: ex b being Element of Domains_of T st S₁[a,b]
reconsider G = a `1 , F = a `2 as Element of Domains_of T ;
F in { H where H is Subset of T : H is condensed } ;
then A2: ex H being Subset of T st
( H = F & H is condensed ) ;
G in { E where E is Subset of T : E is condensed } ;
then ex E being Subset of T st
( E = G & E is condensed ) ;
then (Cl (Int (G /\ F))) /\ (G /\ F) is condensed by A2, Th17;
then (Cl (Int (G /\ F))) /\ (G /\ F) in { E where E is Subset of T : E is condensed } ;
then reconsider b = (Cl (Int (G /\ F))) /\ (G /\ F) as Element of Domains_of T ;
take b ; :: thesis: S₁[a,b]
let A, B be Element of Domains_of T; :: thesis: ( a = [A,B] implies b = (Cl (Int (A /\ B))) /\ (A /\ B) )
assume a = [A,B] ; :: thesis: b = (Cl (Int (A /\ B))) /\ (A /\ B)
then A3: [A,B] = [G,F] by MCART_1:21;
then A4: B = F by XTUPLE_0:1;
A = G by A3, XTUPLE_0:1;
hence b = (Cl (Int (A /\ B))) /\ (A /\ B) by A4; :: thesis: verum

end;

consider h being Function of [:(Domains_of T),(Domains_of T):],(Domains_of T) such that
A5: for a being Element of [:(Domains_of T),(Domains_of T):] holds S₁[a,h . a] from FUNCT_2:sch 3(A1);
take h ; :: thesis: for A, B being Element of Domains_of T holds h . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B)
let A, B be Element of Domains_of T; :: thesis: h . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B)
thus h . (A,B) = h . [A,B]
.= (Cl (Int (A /\ B))) /\ (A /\ B) by A5 ; :: thesis: verum