let L be complete lim-inf TopLattice; :: thesis: ( L is compact & L is T_1 )
set T = the correct Lawson TopAugmentation of L;
now :: thesis: for F being ultra Filter of (BoolePoset ([#] L)) ex x being Point of L st x is_a_convergence_point_of F,L
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:31; :: thesis: L is T_1
now :: thesis: for x being Point of L holds Cl {x} = {x}
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 the correct Lawson TopAugmentation of L, the InternalRel of the correct Lawson TopAugmentation of L #) by YELLOW_9:def 4;
then reconsider z = y as Element of the correct Lawson TopAugmentation of L ;
L is TopAugmentation of L by YELLOW_9:44;
then A1: L is TopExtension of the correct Lawson TopAugmentation of L by Th25;
{z} is closed ;
then {y} is closed by A1, Th23;
hence Cl {x} = {x} by PRE_TOPC:22; :: thesis: verum
end;
hence L is T_1 by FRECHET2:43; :: thesis: verum