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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (uparrow V) where V is Subset of T2 : V in B2 } or z in bool the carrier of T1 )
assume z in { (uparrow V) where V is Subset of T2 : V in B2 } ; :: thesis: z in bool the carrier of T1
then ex V being Subset of T2 st
( z = uparrow V & V in B2 ) ;
hence z in bool the carrier of T1 by A1; :: thesis: verum

end;

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 ;
A2: the topology of T1 c= UniCl upV

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the topology of T1 or z in UniCl upV )
assume A3: z in the topology of T1 ; :: thesis: z in UniCl upV
then reconsider z2 = z as Subset of T1 ;
z2 is open by A3, PRE_TOPC:def 2;
then z2 is upper by WAYBEL11:def 4;
then A4: uparrow z2 c= z2 by WAYBEL_0:24;
reconsider z1 = z as Subset of T2 by A1, A3;
z in sigma T1 by A3, WAYBEL14:23;
then ( sigma T2 c= lambda T2 & z in sigma T2 ) by A1, WAYBEL30:10, YELLOW_9:52;
then z in lambda T2 ;
then z in the topology of T2 by WAYBEL30:9;
then A5: z1 is open by PRE_TOPC:def 2;
{ (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } c= bool the carrier of T1

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } or v in bool the carrier of T1 )
assume v in { (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } ; :: thesis: v in bool the carrier of T1
then ex G being Subset of T2 st
( v = uparrow G & G in B2 & G c= z1 ) ;
hence v in bool the carrier of T1 by A1; :: thesis: verum

end;

then reconsider Y = { (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } as Subset-Family of T1 ;
{ G where G is Subset of T2 : ( G in B2 & G c= z1 ) } c= bool the carrier of T1

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } or v in bool the carrier of T1 )
assume v in { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } ; :: thesis: v in bool the carrier of T1
then ex G being Subset of T2 st
( v = G & G in B2 & G c= z1 ) ;
hence v in bool the carrier of T1 by A1; :: thesis: verum

end;

then reconsider Y1 = { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } as Subset-Family of T1 ;
defpred S₁[ set ] means ( $1 in B2 & $1 c= z1 );
reconsider Y = Y as Subset-Family of T1 ;
reconsider Y1 = Y1 as Subset-Family of T1 ;
reconsider Y3 = Y1 as Subset-Family of T2 by A1;
A6: Y c= upV

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in Y or v in upV )
assume v in Y ; :: thesis: v in upV
then ex G being Subset of T2 st
( v = uparrow G & G in B2 & G c= z1 ) ;
hence v in upV ; :: thesis: verum

end;

A7: for S being Subset-Family of T2 st S = { X where X is Subset of T2 : S₁[X] } holds
uparrow (union S) = union { (uparrow X) where X is Subset of T2 : S₁[X] } from WAYBEL31:sch 1();
z2 c= uparrow z2 by WAYBEL_0:16;
then z1 = uparrow z2 by A4, XBOOLE_0:def 10
.= uparrow (union Y1) by A5, YELLOW_8:9
.= uparrow (union Y3) by A1, WAYBEL_0:13
.= union Y by A7 ;
hence z in UniCl upV by A6, CANTOR_1:def 1; :: thesis: verum

end;

upV c= the topology of T1

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in upV or z in the topology of T1 )
assume z in upV ; :: thesis: z in the topology of T1
then consider V being Subset of T2 such that
A8: z = uparrow V and
A9: V in B2 ;
A10: T1 is Scott TopAugmentation of T2 by A1, YELLOW_9:def 4;
B2 c= the topology of T2 by TOPS_2:64;
then V in the topology of T2 by A9;
then V in lambda T2 by WAYBEL30:9;
then uparrow V in sigma T1 by A10, WAYBEL30:14;
hence z in the topology of T1 by A8, WAYBEL14:23; :: thesis: verum

end;

hence { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1 by A2, CANTOR_1:def 2, TOPS_2:64; :: thesis: verum