let S, T be non empty lower-bounded Poset; for S' being correct lower TopAugmentation of S
for T' being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S',T':]
consider ST being correct lower TopAugmentation of [:S,T:];
reconsider BX = { ((uparrow x) ` ) where x is Element of : verum } as prebasis of ST by Def1;
let S' be correct lower TopAugmentation of S; for T' being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S',T':]
reconsider BS = { ((uparrow x) ` ) where x is Element of : verum } as prebasis of S' by Def1;
let T' be correct lower TopAugmentation of T; omega [:S,T:] = the topology of [:S',T':]
set SxT = [:S',T':];
set B2 = { [:a,the carrier of T':] where a is Subset of : a in BS } ;
A1:
RelStr(# the carrier of T',the InternalRel of T' #) = RelStr(# the carrier of T,the InternalRel of T #)
by YELLOW_9:def 4;
reconsider BT = { ((uparrow x) ` ) where x is Element of : verum } as prebasis of T' by Def1;
A2:
RelStr(# the carrier of S',the InternalRel of S' #) = RelStr(# the carrier of S,the InternalRel of S #)
by YELLOW_9:def 4;
then A3:
the carrier of [:S',T':] = [: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 [:S',T':]
proof
let z be
set ;
TARSKI:def 3 ( not z in BX or z in the topology of [:S',T':] )
A7:
[#] T' is
open
by TOPS_1:53;
assume
z in BX
;
z in the topology of [:S',T':]
then consider x being
Element of
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
by A10;
reconsider s =
s as
Element of
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 s' =
s as
Element of
by A2;
A13:
BS is
open
by YELLOW_9:28;
reconsider t' =
t as
Element of
by A1;
A14:
BT is
open
by YELLOW_9:28;
(uparrow t') ` in BT
;
then A15:
(uparrow t') ` is
open
by A14, TOPS_2:def 1;
reconsider A1 =
[:((uparrow s) ` ),([#] T):],
A2 =
[:([#] S),((uparrow t) ` ):] as
Subset of
by A3, YELLOW_3:def 2;
A16:
[#] S' is
open
by TOPS_1:53;
(uparrow s') ` in BS
;
then A17:
(uparrow s') ` is
open
by A13, TOPS_2:def 1;
uparrow t = uparrow t'
by A1, WAYBEL_0:13;
then A18:
A2 is
open
by A15, A16, A2, A1, BORSUK_1:46;
uparrow s = uparrow s'
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
[:S',T':]
by A12, PRE_TOPC:def 5;
verum
end;
set B1 = { [:the carrier of S',b:] where b is Subset of : b in BT } ;
reconsider BB = { [:the carrier of S',b:] where b is Subset of : b in BT } \/ { [:a,the carrier of T':] where a is Subset of : a in BS } as prebasis of [:S',T':] by YELLOW_9:41;
A19:
UniCl the topology of [:S',T':] = the topology of [:S',T':]
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 S',b:] where b is Subset of : b in BT } or z in { [:a,the carrier of T':] where a is Subset of : a in BS } )
by A20, XBOOLE_0:def 3;
suppose
z in { [:the carrier of S',b:] where b is Subset of : b in BT }
;
z in BXthen consider b being
Subset of
such that A21:
z = [:the carrier of S',b:]
and A22:
b in BT
;
consider t' being
Element of
such that A23:
b = (uparrow t') `
by A22;
reconsider t =
t' as
Element of
by A1;
reconsider x =
[(Bottom S),t] as
Element of
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 t'
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 T':] where a is Subset of : a in BS }
;
z in BXthen consider a being
Subset of
such that A26:
z = [:a,the carrier of T':]
and A27:
a in BS
;
consider s' being
Element of
such that A28:
a = (uparrow s') `
by A27;
reconsider s =
s' as
Element of
by A2;
reconsider x =
[s,(Bottom T)] as
Element of
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 s'
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 [:S',T':]
by YELLOW_9:23;
then A32:
the topology of [:S',T':] = 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 [:S',T':] = the topology of [:S',T':]
by CANTOR_1:5;
then
FinMeetCl BX c= the topology of [:S',T':]
by A6, A5, A3, CANTOR_1:16;
then
UniCl (FinMeetCl BX) c= the topology of [:S',T':]
by A5, A3, A19, CANTOR_1:9;
then
the topology of ST = the topology of [:S',T':]
by A33, A32, A31, XBOOLE_0:def 10;
hence
omega [:S,T:] = the topology of [:S',T':]
by Def2; verum