let L be Semilattice; :: thesis: for F being Filter of L holds F = uparrow (fininfs F)
let F be Filter of L; :: thesis: F = uparrow (fininfs F)
thus F c= uparrow (fininfs F) by WAYBEL_0:62; :: according to XBOOLE_0:def 10 :: thesis: uparrow (fininfs F) c= F
thus uparrow (fininfs F) c= F by WAYBEL_0:62; :: thesis: verum