let L be complete lim-inf TopLattice; :: thesis: ( L is compact & L is T_1 )

now

let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: ex x being Point of L st x is_a_convergence_point_of F,L
reconsider x = lim_inf F as Point of L ;
take x = x; :: thesis: x is_a_convergence_point_of F,L
thus x is_a_convergence_point_of F,L by Th26; :: thesis: verum

end;

hence L is compact by YELLOW19:33; :: thesis: L is T_1
consider T being correct Lawson TopAugmentation of L;

now

let x be Point of L; :: thesis: Cl {x} = {x}
reconsider y = x as Element of L ;
RelStr(# the carrier of L,the InternalRel of L #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
then reconsider z = y as Element of T ;
L is TopAugmentation of L by YELLOW_9:44;
then ( L is TopExtension of T & {z} is closed ) by Th25;
then {y} is closed by Th23;
hence Cl {x} = {x} by PRE_TOPC:52; :: thesis: verum

end;

hence L is T_1 by FRECHET2:47; :: thesis: verum