let L be complete LATTICE; :: thesis: for T being lim-inf TopAugmentation of L
for S being correct Lawson TopAugmentation of L holds T is TopExtension of S
let T be lim-inf TopAugmentation of L; :: thesis: for S being correct Lawson TopAugmentation of L holds T is TopExtension of S
let S be correct Lawson TopAugmentation of L; :: thesis: T is TopExtension of S
( lambda L = the topology of S & xi L = the topology of T ) by Th10, WAYBEL19:def 4;
then A1: the topology of S c= the topology of T by Th24;
( RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def 4;
hence T is TopExtension of S by A1, YELLOW_9:def 5; :: thesis: verum