let L be with_suprema Poset; :: thesis: for X being Subset of L holds
( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds
downarrow (finsups X) c= I ) )
let X be Subset of L; :: thesis: ( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds
downarrow (finsups X) c= I ) )
( X c= finsups X & finsups X c= downarrow (finsups X) ) by Th16, Th50;
hence X c= downarrow (finsups X) by XBOOLE_1:1; :: thesis: for I being Ideal of L st X c= I holds
downarrow (finsups X) c= I
let I be Ideal of L; :: thesis: ( X c= I implies downarrow (finsups X) c= I )
assume A1: X c= I ; :: thesis: downarrow (finsups X) c= I
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow (finsups X) or x in I )
assume A2: x in downarrow (finsups X) ; :: thesis: x in I
then reconsider x = x as Element of L ;
consider y being Element of L such that
A3: ( x <= y & y in finsups X ) by A2, Def15;
consider Y being finite Subset of X such that
A4: ( y = "\/" Y,L & ex_sup_of Y,L ) by A3;
consider i being Element of I;
reconsider i = i as Element of L ;
A5: ( ex_sup_of {i},L & sup {i} = i & {} c= {i} ) by XBOOLE_1:2, YELLOW_0:38, YELLOW_0:39;

A6: now

assume ex_sup_of {} ,L ; :: thesis: "\/" {} ,L in I
then "\/" {} ,L <= sup {i} by A5, YELLOW_0:34;
hence "\/" {} ,L in I by A5, Def19; :: thesis: verum

end;

( Y c= I & ( Y = {} or Y <> {} ) ) by A1, XBOOLE_1:1;
then y in I by A4, A6, Th42;
hence x in I by A3, Def19; :: thesis: verum