defpred S₁[ set , set ] means for A, B being Element of Closed_Domains_of T st $1 = [A,B] holds
$2 = 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 S₁[a,b]

proof

let a be Element of [:(Closed_Domains_of T),(Closed_Domains_of T):]; :: thesis: ex b being Element of Closed_Domains_of T st S₁[a,b]
reconsider G = a `1 , F = a `2 as Element of Closed_Domains_of T ;
G in { E where E is Subset of T : E is closed_condensed } ;
then consider E being Subset of T such that
A2: E = G and
A3: E is closed_condensed ;
F in { H where H is Subset of T : H is closed_condensed } ;
then consider H being Subset of T such that
A4: H = F and
A5: H is closed_condensed ;
E \/ H is closed_condensed by A3, A5, TOPS_1:108;
then G \/ F in { K where K is Subset of T : K is closed_condensed } by A2, A4;
then reconsider b = G \/ F as Element of Closed_Domains_of T ;
take b ; :: thesis: S₁[a,b]
let A, B be Element of Closed_Domains_of T; :: thesis: ( a = [A,B] implies b = A \/ B )
assume a = [A,B] ; :: thesis: b = A \/ B
then A6: [A,B] = [G,F] by MCART_1:23;
then A = G by ZFMISC_1:33;
hence b = A \/ B by A6, ZFMISC_1:33; :: thesis: verum

end;

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