let L1 be lower-bounded continuous sup-Semilattice; :: thesis: for T1 being Scott TopAugmentation of L1
for T2 being correct Lawson TopAugmentation of L1
for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
let T1 be Scott TopAugmentation of L1; :: thesis: for T2 being correct Lawson TopAugmentation of L1
for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
let T2 be correct Lawson TopAugmentation of L1; :: thesis: for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
let B2 be Basis of T2; :: thesis: { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
A1:
( RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of L1,the InternalRel of L1 #) & RelStr(# the carrier of T2,the InternalRel of T2 #) = RelStr(# the carrier of L1,the InternalRel of L1 #) )
by YELLOW_9:def 4;
{ (uparrow V) where V is Subset of T2 : V in B2 } c= bool the carrier of T1
then reconsider upV = { (uparrow V) where V is Subset of T2 : V in B2 } as Subset-Family of T1 ;
reconsider upV = upV as Subset-Family of T1 ;
A3:
upV c= the topology of T1
the topology of T1 c= UniCl upV
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in the topology of T1 or z in UniCl upV )
assume A7:
z in the
topology of
T1
;
:: thesis: z in UniCl upV
then reconsider z2 =
z as
Subset of
T1 ;
A8:
z in sigma T1
by A7, WAYBEL14:23;
A9:
sigma T2 c= lambda T2
by WAYBEL30:10;
z in sigma T2
by A1, A8, YELLOW_9:52;
then
z in lambda T2
by A9;
then A10:
z in the
topology of
T2
by WAYBEL30:9;
reconsider z1 =
z as
Subset of
T2 by A1, A7;
{ G where G is Subset of T2 : ( G in B2 & G c= z1 ) } c= bool the
carrier of
T1
then reconsider Y1 =
{ G where G is Subset of T2 : ( G in B2 & G c= z1 ) } as
Subset-Family of
T1 ;
reconsider Y1 =
Y1 as
Subset-Family of
T1 ;
reconsider Y3 =
Y1 as
Subset-Family of
T2 by A1;
{ (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } c= bool the
carrier of
T1
then reconsider Y =
{ (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } as
Subset-Family of
T1 ;
reconsider Y =
Y as
Subset-Family of
T1 ;
A13:
z1 is
open
by A10, PRE_TOPC:def 5;
z2 is
open
by A7, PRE_TOPC:def 5;
then
z2 is
upper
by WAYBEL11:def 4;
then A14:
uparrow z2 c= z2
by WAYBEL_0:24;
defpred S1[
set ]
means ( $1
in B2 & $1
c= z1 );
A15:
for
S being
Subset-Family of
T2 st
S = { X where X is Subset of T2 : S1[X] } holds
uparrow (union S) = union { (uparrow X) where X is Subset of T2 : S1[X] }
from WAYBEL31:sch 1();
z2 c= uparrow z2
by WAYBEL_0:16;
then A16:
z1 =
uparrow z2
by A14, XBOOLE_0:def 10
.=
uparrow (union Y1)
by A13, YELLOW_8:18
.=
uparrow (union Y3)
by A1, WAYBEL_0:13
.=
union Y
by A15
;
Y c= upV
hence
z in UniCl upV
by A16, CANTOR_1:def 1;
:: thesis: verum
end;
hence
{ (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
by A3, CANTOR_1:def 2; :: thesis: verum