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

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