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 A1: A is open ; :: thesis: for C being Subset of S st C = A holds
C is open
let C be Subset of S; :: thesis: ( C = A implies C is open )
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
assume C = A ; :: thesis: C is open
then ( C is upper & C is property(S) ) by A1, Th36, A2, WAYBEL_0:25, YELLOW12:19;
hence C is open by WAYBEL11:15; :: thesis: verum