set D = [:(Closed_Domains_of T),(Closed_Domains_of T):];
defpred S1[ set , set ] means for A, B being Element of Closed_Domains_of T st $1 = [A,B] holds
$2 = A \/ B;
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):];
:: thesis: 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 ;
A2:
(
G in { E where E is Subset of T : E is closed_condensed } &
F in { H where H is Subset of T : H is closed_condensed } )
;
then consider E being
Subset of
T such that A3:
(
E = G &
E is
closed_condensed )
;
consider H being
Subset of
T such that A4:
(
H = F &
H is
closed_condensed )
by A2;
E \/ H is
closed_condensed
by A3, A4, TOPS_1:108;
then
G \/ F in { K where K is Subset of T : K is closed_condensed }
by A3, A4;
then reconsider b =
G \/ F as
Element of
Closed_Domains_of T ;
take
b
;
:: thesis: S1[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
[A,B] = [G,F]
by MCART_1:23;
then
(
A = G &
B = F )
by ZFMISC_1:33;
hence
b = A \/ B
;
:: thesis: verum
end;
consider h being Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Closed_Domains_of T) such that
A5:
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
; :: 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 A5
; :: thesis: verum