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:]
consider ST being correct lower TopAugmentation of [:S,T:];
reconsider BX = { ((uparrow x) ` ) where x is Element of ST : verum } as prebasis of ST 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 5;
A4:
RelStr(# the carrier of ST,the InternalRel of ST #) = [:S,T:]
by YELLOW_9:def 4;
then A5:
the carrier of ST = [: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
set ;
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
ST such that A8:
z = (uparrow x) `
;
consider s,
t being
set 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 A15:
(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;
A16:
[#] S9 is
open
;
(uparrow s9) ` in BS
;
then A17:
(uparrow s9) ` is
open
by TOPS_2:def 1;
uparrow t = uparrow t9
by A1, WAYBEL_0:13;
then A18:
A2 is
open
by A15, A16, A2, A1, BORSUK_1:46;
uparrow s = uparrow s9
by A2, WAYBEL_0:13;
then
A1 is
open
by A17, A7, A2, A1, BORSUK_1:46;
then
A1 \/ A2 is
open
by A18, TOPS_1:37;
hence
z in the
topology of
[:S9,T9:]
by A12, PRE_TOPC:def 5;
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;
A19:
UniCl the topology of [:S9,T9:] = the topology of [:S9,T9:]
by CANTOR_1:6;
BB c= BX
proof
let z be
set ;
TARSKI:def 3 ( not z in BB or z in BX )
assume A20:
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 A20, 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 A21:
z = [:the carrier of S9,b:]
and A22:
b in BT
;
consider t9 being
Element of
T9 such that A23:
b = (uparrow t9) `
by A22;
reconsider t =
t9 as
Element of
T by A1;
reconsider x =
[(Bottom S),t] as
Element of
ST by A4;
A24:
uparrow x = uparrow [(Bottom S),t]
by A4, WAYBEL_0:13;
uparrow (Bottom S) = the
carrier of
S
by WAYBEL14:10;
then A25:
(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 A25, A1, A23, Th14
.=
{} \/ [:the carrier of S,b:]
by ZFMISC_1:113
.=
z
by A2, A21
;
hence
z in BX
by A4, A24;
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 A26:
z = [:a,the carrier of T9:]
and A27:
a in BS
;
consider s9 being
Element of
S9 such that A28:
a = (uparrow s9) `
by A27;
reconsider s =
s9 as
Element of
S by A2;
reconsider x =
[s,(Bottom T)] as
Element of
ST by A4;
A29:
uparrow x = uparrow [s,(Bottom T)]
by A4, WAYBEL_0:13;
uparrow (Bottom T) = the
carrier of
T
by WAYBEL14:10;
then A30:
(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 A30, A2, A28, Th14
.=
[:a,the carrier of T:] \/ {}
by ZFMISC_1:113
.=
z
by A1, A26
;
hence
z in BX
by A4, A29;
verum end;
end;
then
FinMeetCl BB c= FinMeetCl BX
by A5, A3, CANTOR_1:16;
then A31:
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 A32:
the topology of [:S9,T9:] = UniCl (FinMeetCl BB)
by YELLOW_9:22;
FinMeetCl BX is Basis of ST
by YELLOW_9:23;
then A33:
the topology of ST = 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:16;
then
UniCl (FinMeetCl BX) c= the topology of [:S9,T9:]
by A5, A3, A19, CANTOR_1:9;
then
the topology of ST = the topology of [:S9,T9:]
by A33, A32, A31, XBOOLE_0:def 10;
hence
omega [:S,T:] = the topology of [:S9,T9:]
by Def2; verum