let L be complete lim-inf TopLattice; :: thesis: for F being ultra Filter of (BoolePoset ([#] L)) holds lim_inf F is_a_convergence_point_of F,L

let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: lim_inf F is_a_convergence_point_of F,L

set x = lim_inf F;

let A be Subset of L; :: according to WAYBEL_7:def 5 :: thesis: ( not A is open or not lim_inf F in A or A in F )

assume that

A1: A is open and

A2: lim_inf F in A and

A3: not A in F ; :: thesis: contradiction

F is prime by WAYBEL_7:22;

then A4: ([#] L) \ A in F by A3, WAYBEL_7:21;

then A ` <> {} by YELLOW19:1;

then lim_inf F in A ` by A1, A4, Th18;

hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: lim_inf F is_a_convergence_point_of F,L

set x = lim_inf F;

let A be Subset of L; :: according to WAYBEL_7:def 5 :: thesis: ( not A is open or not lim_inf F in A or A in F )

assume that

A1: A is open and

A2: lim_inf F in A and

A3: not A in F ; :: thesis: contradiction

F is prime by WAYBEL_7:22;

then A4: ([#] L) \ A in F by A3, WAYBEL_7:21;

then A ` <> {} by YELLOW19:1;

then lim_inf F in A ` by A1, A4, Th18;

hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum