let S, T be non empty lower-bounded Poset; for S9 being correct lower TopAugmentation of S
for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:]
set ST = the correct lower TopAugmentation of [:S,T:];
reconsider BX = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of [:S,T:] : verum } as prebasis of the correct lower TopAugmentation of [:S,T:] by Def1;
let S9 be correct lower TopAugmentation of S; for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:]
reconsider BS = { ((uparrow x) `) where x is Element of S9 : verum } as prebasis of S9 by Def1;
let T9 be correct lower TopAugmentation of T; omega [:S,T:] = the topology of [:S9,T9:]
set SxT = [:S9,T9:];
set B2 = { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } ;
A1:
RelStr(# the carrier of T9, the InternalRel of T9 #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
reconsider BT = { ((uparrow x) `) where x is Element of T9 : verum } as prebasis of T9 by Def1;
A2:
RelStr(# the carrier of S9, the InternalRel of S9 #) = RelStr(# the carrier of S, the InternalRel of S #)
by YELLOW_9:def 4;
then A3:
the carrier of [:S9,T9:] = [: the carrier of S, the carrier of T:]
by A1, BORSUK_1:def 2;
A4:
RelStr(# the carrier of the correct lower TopAugmentation of [:S,T:], the InternalRel of the correct lower TopAugmentation of [:S,T:] #) = [:S,T:]
by YELLOW_9:def 4;
then A5:
the carrier of the correct lower TopAugmentation of [:S,T:] = [: the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
A6:
BX c= the topology of [:S9,T9:]
proof
let z be
object ;
TARSKI:def 3 ( not z in BX or z in the topology of [:S9,T9:] )
A7:
[#] T9 is
open
;
assume
z in BX
;
z in the topology of [:S9,T9:]
then consider x being
Element of the
correct lower TopAugmentation of
[:S,T:] such that A8:
z = (uparrow x) `
;
consider s,
t being
object such that A9:
s in the
carrier of
S
and A10:
t in the
carrier of
T
and A11:
x = [s,t]
by A5, ZFMISC_1:def 2;
reconsider t =
t as
Element of
T by A10;
reconsider s =
s as
Element of
S by A9;
uparrow x = uparrow [s,t]
by A4, A11, WAYBEL_0:13;
then A12:
z = [:((uparrow s) `),([#] T):] \/ [:([#] S),((uparrow t) `):]
by A4, A8, Th14;
reconsider s9 =
s as
Element of
S9 by A2;
reconsider t9 =
t as
Element of
T9 by A1;
(uparrow t9) ` in BT
;
then A13:
(uparrow t9) ` is
open
by TOPS_2:def 1;
reconsider A1 =
[:((uparrow s) `),([#] T):],
A2 =
[:([#] S),((uparrow t) `):] as
Subset of
[:S9,T9:] by A3, YELLOW_3:def 2;
A14:
[#] S9 is
open
;
(uparrow s9) ` in BS
;
then A15:
(uparrow s9) ` is
open
by TOPS_2:def 1;
uparrow t = uparrow t9
by A1, WAYBEL_0:13;
then A16:
A2 is
open
by A13, A14, A2, A1, BORSUK_1:6;
uparrow s = uparrow s9
by A2, WAYBEL_0:13;
then
A1 is
open
by A15, A7, A2, A1, BORSUK_1:6;
then
A1 \/ A2 is
open
by A16;
hence
z in the
topology of
[:S9,T9:]
by A12;
verum
end;
set B1 = { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } ;
reconsider BB = { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } \/ { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } as prebasis of [:S9,T9:] by YELLOW_9:41;
A17:
UniCl the topology of [:S9,T9:] = the topology of [:S9,T9:]
by CANTOR_1:6;
BB c= BX
proof
let z be
object ;
TARSKI:def 3 ( not z in BB or z in BX )
assume A18:
z in BB
;
z in BX
per cases
( z in { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } or z in { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } )
by A18, XBOOLE_0:def 3;
suppose
z in { [: the carrier of S9,b:] where b is Subset of T9 : b in BT }
;
z in BXthen consider b being
Subset of
T9 such that A19:
z = [: the carrier of S9,b:]
and A20:
b in BT
;
consider t9 being
Element of
T9 such that A21:
b = (uparrow t9) `
by A20;
reconsider t =
t9 as
Element of
T by A1;
reconsider x =
[(Bottom S),t] as
Element of the
correct lower TopAugmentation of
[:S,T:] by A4;
A22:
uparrow x = uparrow [(Bottom S),t]
by A4, WAYBEL_0:13;
uparrow (Bottom S) = the
carrier of
S
by WAYBEL14:10;
then A23:
(uparrow (Bottom S)) ` = {}
by XBOOLE_1:37;
uparrow t = uparrow t9
by A1, WAYBEL_0:13;
then (uparrow [(Bottom S),t]) ` =
[:{}, the carrier of T:] \/ [: the carrier of S,b:]
by A23, A1, A21, Th14
.=
{} \/ [: the carrier of S,b:]
by ZFMISC_1:90
.=
z
by A2, A19
;
hence
z in BX
by A4, A22;
verum end; suppose
z in { [:a, the carrier of T9:] where a is Subset of S9 : a in BS }
;
z in BXthen consider a being
Subset of
S9 such that A24:
z = [:a, the carrier of T9:]
and A25:
a in BS
;
consider s9 being
Element of
S9 such that A26:
a = (uparrow s9) `
by A25;
reconsider s =
s9 as
Element of
S by A2;
reconsider x =
[s,(Bottom T)] as
Element of the
correct lower TopAugmentation of
[:S,T:] by A4;
A27:
uparrow x = uparrow [s,(Bottom T)]
by A4, WAYBEL_0:13;
uparrow (Bottom T) = the
carrier of
T
by WAYBEL14:10;
then A28:
(uparrow (Bottom T)) ` = {}
by XBOOLE_1:37;
uparrow s = uparrow s9
by A2, WAYBEL_0:13;
then (uparrow [s,(Bottom T)]) ` =
[:a, the carrier of T:] \/ [: the carrier of S,{}:]
by A28, A2, A26, Th14
.=
[:a, the carrier of T:] \/ {}
by ZFMISC_1:90
.=
z
by A1, A24
;
hence
z in BX
by A4, A27;
verum end;
end;
then
FinMeetCl BB c= FinMeetCl BX
by A5, A3, CANTOR_1:14;
then A29:
UniCl (FinMeetCl BB) c= UniCl (FinMeetCl BX)
by A5, A3, CANTOR_1:9;
FinMeetCl BB is Basis of [:S9,T9:]
by YELLOW_9:23;
then A30:
the topology of [:S9,T9:] = UniCl (FinMeetCl BB)
by YELLOW_9:22;
FinMeetCl BX is Basis of the correct lower TopAugmentation of [:S,T:]
by YELLOW_9:23;
then A31:
the topology of the correct lower TopAugmentation of [:S,T:] = UniCl (FinMeetCl BX)
by YELLOW_9:22;
FinMeetCl the topology of [:S9,T9:] = the topology of [:S9,T9:]
by CANTOR_1:5;
then
FinMeetCl BX c= the topology of [:S9,T9:]
by A6, A5, A3, CANTOR_1:14;
then
UniCl (FinMeetCl BX) c= the topology of [:S9,T9:]
by A5, A3, A17, CANTOR_1:9;
then
the topology of the correct lower TopAugmentation of [:S,T:] = the topology of [:S9,T9:]
by A31, A30, A29;
hence
omega [:S,T:] = the topology of [:S9,T9:]
by Def2; verum