set D = [:(Open_Domains_of T),(Open_Domains_of T):];
defpred S1[ set , set ] means for A, B being Element of Open_Domains_of T st $1 = [A,B] holds
$2 = A /\ B;
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):];
:: thesis: 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 ;
A2:
(
G in { E where E is Subset of T : E is open_condensed } &
F in { H where H is Subset of T : H is open_condensed } )
;
then consider E being
Subset of
T such that A3:
(
E = G &
E is
open_condensed )
;
consider H being
Subset of
T such that A4:
(
H = F &
H is
open_condensed )
by A2;
E /\ H is
open_condensed
by A3, A4, TOPS_1:109;
then
G /\ F in { K where K is Subset of T : K is open_condensed }
by A3, A4;
then reconsider b =
G /\ F as
Element of
Open_Domains_of T ;
take
b
;
:: thesis: S1[a,b]
let A,
B be
Element of
Open_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 [:(Open_Domains_of T),(Open_Domains_of T):],(Open_Domains_of T) such that
A5:
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
; :: thesis: 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; :: thesis: h . A,B = A /\ B
thus h . A,B =
h . [A,B]
.=
A /\ B
by A5
; :: thesis: verum