let L be with_infima Poset; :: thesis: for X being Subset of L holds
( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds
uparrow (fininfs X) c= F ) )
let X be Subset of L; :: thesis: ( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds
uparrow (fininfs X) c= F ) )
A1: X c= fininfs X by Th50;
fininfs X c= uparrow (fininfs X) by Th16;
hence X c= uparrow (fininfs X) by A1, XBOOLE_1:1; :: thesis: for F being Filter of L st X c= F holds
uparrow (fininfs X) c= F
let I be Filter of L; :: thesis: ( X c= I implies uparrow (fininfs X) c= I )
assume A2: X c= I ; :: thesis: uparrow (fininfs X) c= I
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow (fininfs X) or x in I )
assume A3: x in uparrow (fininfs X) ; :: thesis: x in I
then reconsider x = x as Element of L ;
consider y being Element of L such that
A4: x >= y and
A5: y in fininfs X by A3, Def16;
consider Y being finite Subset of X such that
A6: y = "/\" Y,L and
A7: ex_inf_of Y,L by A5;
consider i being Element of I;
reconsider i = i as Element of L ;
A8: ex_inf_of {i},L by YELLOW_0:38;
A9: inf {i} = i by YELLOW_0:39;

A10: now

assume ex_inf_of {} ,L ; :: thesis: "/\" {} ,L in I
then "/\" {} ,L >= inf {i} by A8, XBOOLE_1:2, YELLOW_0:35;
hence "/\" {} ,L in I by A9, Def20; :: thesis: verum

end;

Y c= I by A2, XBOOLE_1:1;
then y in I by A6, A7, A10, Th43;
hence x in I by A4, Def20; :: thesis: verum