defpred S1[ set , set ] means for A, B being Element of Open_Domains_of T st $1 = [A,B] holds
$2 = 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 ;
G in { E where E is Subset of T : E is open_condensed }
;
then consider E being
Subset of
T such that A2:
E = G
and A3:
E is
open_condensed
;
F in { H where H is Subset of T : H is open_condensed }
;
then consider H being
Subset of
T such that A4:
H = F
and A5:
H is
open_condensed
;
E /\ H is
open_condensed
by A3, A5, TOPS_1:69;
then
G /\ F in { K where K is Subset of T : K is open_condensed }
by A2, A4;
then reconsider b =
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 = A /\ B )
assume
a = [A,B]
;
b = A /\ B
then A6:
[A,B] = [G,F]
by MCART_1:21;
then
A = G
by XTUPLE_0:1;
hence
b = A /\ B
by A6, XTUPLE_0:1;
verum
end;
consider h being Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Open_Domains_of T) such that
A7:
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) = A /\ B
let A, B be Element of Open_Domains_of T; h . (A,B) = A /\ B
thus h . (A,B) =
h . [A,B]
.=
A /\ B
by A7
; verum