let L be up-complete /\-complete Semilattice; :: thesis: for X being lim-inf TopAugmentation of L holds xi L = the topology of X
let X be lim-inf TopAugmentation of L; :: thesis: xi L = the topology of X
( the topology of X = xi X & RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of L, the InternalRel of L #) ) by Def2, YELLOW_9:def 4;
hence xi L = the topology of X by Th9; :: thesis: verum