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
A1: lambda L = the topology of S by WAYBEL19:def 4;
A2: ( 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;
xi L = the topology of T by Th10;
then the topology of S c= the topology of T by A1, Th24;
hence T is TopExtension of S by A2, YELLOW_9:def 5; :: thesis: verum