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

set T = the correct Lawson TopAugmentation of L;

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

hence
L is compact
by YELLOW19:31; :: thesis: L is T_1 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;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

now :: thesis: for x being Point of L holds Cl {x} = {x}

hence
L is T_1
by FRECHET2:43; :: thesis: verumlet 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;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