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 ) )

A1: X c= finsups X by Th50;

finsups X c= downarrow (finsups X) by Th16;

hence X c= downarrow (finsups X) by A1; :: 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 A2: X c= I ; :: thesis: downarrow (finsups X) c= I

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow (finsups X) or x in I )

assume A3: 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

A4: x <= y and

A5: y in finsups X by A3, Def15;

consider Y being finite Subset of X such that

A6: y = "\/" (Y,L) and

A7: ex_sup_of Y,L by A5;

set i = the Element of I;

reconsider i = the Element of I as Element of L ;

A8: ex_sup_of {i},L by YELLOW_0:38;

A9: sup {i} = i by YELLOW_0:39;

then y in I by A6, A7, A10, Th42;

hence x in I by A4, Def19; :: thesis: verum

( 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 ) )

A1: X c= finsups X by Th50;

finsups X c= downarrow (finsups X) by Th16;

hence X c= downarrow (finsups X) by A1; :: 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 A2: X c= I ; :: thesis: downarrow (finsups X) c= I

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow (finsups X) or x in I )

assume A3: 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

A4: x <= y and

A5: y in finsups X by A3, Def15;

consider Y being finite Subset of X such that

A6: y = "\/" (Y,L) and

A7: ex_sup_of Y,L by A5;

set i = the Element of I;

reconsider i = the Element of I as Element of L ;

A8: ex_sup_of {i},L by YELLOW_0:38;

A9: sup {i} = i by YELLOW_0:39;

A10: now :: thesis: ( ex_sup_of {} ,L implies "\/" ({},L) in I )

Y c= I
by A2;assume
ex_sup_of {} ,L
; :: thesis: "\/" ({},L) in I

then "\/" ({},L) <= sup {i} by A8, XBOOLE_1:2, YELLOW_0:34;

hence "\/" ({},L) in I by A9, Def19; :: thesis: verum

end;then "\/" ({},L) <= sup {i} by A8, XBOOLE_1:2, YELLOW_0:34;

hence "\/" ({},L) in I by A9, Def19; :: thesis: verum

then y in I by A6, A7, A10, Th42;

hence x in I by A4, Def19; :: thesis: verum