let S, T be non empty lower-bounded Poset; :: thesis: 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':]
let S' be correct lower TopAugmentation of S; :: thesis: for T' being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S',T':]
let T' be correct lower TopAugmentation of T; :: thesis: omega [:S,T:] = the topology of [:S',T':]
set SxT = [:S',T':];
reconsider BS = { ((uparrow x) ` ) where x is Element of S' : verum } as prebasis of S' by Def1;
reconsider BT = { ((uparrow x) ` ) where x is Element of T' : verum } as prebasis of T' by Def1;
set B1 = { [:the carrier of S',b:] where b is Subset of T' : b in BT } ;
set B2 = { [:a,the carrier of T':] where a is Subset of S' : a in BS } ;
reconsider BB = { [:the carrier of S',b:] where b is Subset of T' : b in BT } \/ { [:a,the carrier of T':] where a is Subset of S' : a in BS } as prebasis of [:S',T':] by YELLOW_9:41;
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;
A1: ( RelStr(# the carrier of S',the InternalRel of S' #) = RelStr(# the carrier of S,the InternalRel of S #) & RelStr(# the carrier of T',the InternalRel of T' #) = RelStr(# the carrier of T,the InternalRel of T #) & RelStr(# the carrier of ST,the InternalRel of ST #) = [:S,T:] ) by YELLOW_9:def 4;
then A2: the carrier of ST = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
A3: the carrier of [:S',T':] = [:the carrier of S,the carrier of T:] by A1, BORSUK_1:def 5;
BB c= BX

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in BB or z in BX )
assume A4: z in BB ; :: thesis: z in BX

per cases ( z in { [:the carrier of S',b:] where b is Subset of T' : b in BT } or z in { [:a,the carrier of T':] where a is Subset of S' : a in BS } ) by A4, XBOOLE_0:def 3;

suppose z in { [:the carrier of S',b:] where b is Subset of T' : b in BT } ; :: thesis: z in BX

then consider b being Subset of T' such that
A5: ( z = [:the carrier of S',b:] & b in BT ) ;
consider t' being Element of T' such that
A6: b = (uparrow t') ` by A5;
reconsider t = t' as Element of T by A1;
A7: uparrow t = uparrow t' by A1, WAYBEL_0:13;
reconsider x = [(Bottom S),t] as Element of ST by A1;
A8: uparrow x = uparrow [(Bottom S),t] by A1, WAYBEL_0:13;
uparrow (Bottom S) = the carrier of S by WAYBEL14:10;
then (uparrow (Bottom S)) ` = {} by XBOOLE_1:37;
then (uparrow [(Bottom S),t]) ` = [:{} ,the carrier of T:] \/ [:the carrier of S,b:] by A1, A6, A7, Th14
.= {} \/ [:the carrier of S,b:] by ZFMISC_1:113
.= z by A1, A5 ;
hence z in BX by A1, A8; :: thesis: verum

end;

suppose z in { [:a,the carrier of T':] where a is Subset of S' : a in BS } ; :: thesis: z in BX

then consider a being Subset of S' such that
A9: ( z = [:a,the carrier of T':] & a in BS ) ;
consider s' being Element of S' such that
A10: a = (uparrow s') ` by A9;
reconsider s = s' as Element of S by A1;
A11: uparrow s = uparrow s' by A1, WAYBEL_0:13;
reconsider x = [s,(Bottom T)] as Element of ST by A1;
A12: uparrow x = uparrow [s,(Bottom T)] by A1, WAYBEL_0:13;
uparrow (Bottom T) = the carrier of T by WAYBEL14:10;
then (uparrow (Bottom T)) ` = {} by XBOOLE_1:37;
then (uparrow [s,(Bottom T)]) ` = [:a,the carrier of T:] \/ [:the carrier of S,{} :] by A1, A10, A11, Th14
.= [:a,the carrier of T:] \/ {} by ZFMISC_1:113
.= z by A1, A9 ;
hence z in BX by A1, A12; :: thesis: verum

end;

end;

end;

then FinMeetCl BB c= FinMeetCl BX by A2, A3, CANTOR_1:16;
then A13: UniCl (FinMeetCl BB) c= UniCl (FinMeetCl BX) by A2, A3, CANTOR_1:9;
A14: ( FinMeetCl the topology of ST = the topology of ST & FinMeetCl the topology of [:S',T':] = the topology of [:S',T':] ) by CANTOR_1:5;
A15: ( UniCl the topology of ST = the topology of ST & UniCl the topology of [:S',T':] = the topology of [:S',T':] ) by CANTOR_1:6;
BX c= the topology of [:S',T':]

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in BX or z in the topology of [:S',T':] )
assume z in BX ; :: thesis: z in the topology of [:S',T':]
then consider x being Element of ST such that
A16: z = (uparrow x) ` ;
consider s, t being set such that
A17: ( s in the carrier of S & t in the carrier of T & x = [s,t] ) by A2, ZFMISC_1:def 2;
reconsider s = s as Element of S by A17;
reconsider t = t as Element of T by A17;
reconsider s' = s as Element of S' by A1;
reconsider t' = t as Element of T' by A1;
uparrow x = uparrow [s,t] by A1, A17, WAYBEL_0:13;
then A18: z = [:((uparrow s) ` ),([#] T):] \/ [:([#] S),((uparrow t) ` ):] by A1, A16, Th14;
A19: ( uparrow s = uparrow s' & uparrow t = uparrow t' ) by A1, WAYBEL_0:13;
reconsider A1 = [:((uparrow s) ` ),([#] T):], A2 = [:([#] S),((uparrow t) ` ):] as Subset of [:S',T':] by A3, YELLOW_3:def 2;
( (uparrow s') ` in BS & (uparrow t') ` in BT & BS is open & BT is open ) by YELLOW_9:28;
then ( (uparrow s') ` is open & (uparrow t') ` is open & [#] S' is open & [#] T' is open ) by TOPS_1:53, TOPS_2:def 1;
then ( A1 is open & A2 is open ) by A1, A19, BORSUK_1:46;
then A1 \/ A2 is open by TOPS_1:37;
hence z in the topology of [:S',T':] by A18, PRE_TOPC:def 5; :: thesis: verum

end;

then FinMeetCl BX c= the topology of [:S',T':] by A2, A3, A14, CANTOR_1:16;
then A20: UniCl (FinMeetCl BX) c= the topology of [:S',T':] by A2, A3, A15, CANTOR_1:9;
( FinMeetCl BX is Basis of ST & FinMeetCl BB is Basis of [:S',T':] ) by YELLOW_9:23;
then ( the topology of ST = UniCl (FinMeetCl BX) & the topology of [:S',T':] = UniCl (FinMeetCl BB) ) by YELLOW_9:22;
then the topology of ST = the topology of [:S',T':] by A13, A20, XBOOLE_0:def 10;
hence omega [:S,T:] = the topology of [:S',T':] by Def2; :: thesis: verum