let S be complete Scott TopLattice; :: thesis: for T being correct Lawson TopAugmentation of S
for A being upper Subset of T st A is open holds
for C being Subset of S st C = A holds
C is open
let T be correct Lawson TopAugmentation of S; :: thesis: for A being upper Subset of T st A is open holds
for C being Subset of S st C = A holds
C is open
let A be upper Subset of T; :: thesis: ( A is open implies for C being Subset of S st C = A holds
C is open )
assume A is open ; :: thesis: for C being Subset of S st C = A holds
C is open
then A1: ( A is property(S) & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of S,the InternalRel of S #) ) by Th36, YELLOW_9:def 4;
let C be Subset of S; :: thesis: ( C = A implies C is open )
assume C = A ; :: thesis: C is open
then ( C is upper & C is property(S) ) by A1, WAYBEL_0:25, YELLOW12:19;
hence C is open by WAYBEL11:15; :: thesis: verum