let L be with_suprema Poset; :: thesis: for I being Ideal of L
for X being non empty finite Subset of L
for x being Element of L st x in downarrow (finsups (I \/ X)) holds
ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
let I be Ideal of L; :: thesis: for X being non empty finite Subset of L
for x being Element of L st x in downarrow (finsups (I \/ X)) holds
ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
let X be non empty finite Subset of L; :: thesis: for x being Element of L st x in downarrow (finsups (I \/ X)) holds
ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
let x be Element of L; :: thesis: ( x in downarrow (finsups (I \/ X)) implies ex i being Element of L st
( i in I & x <= i "\/" (sup X) ) )
set i = the Element of I;
reconsider i = the Element of I as Element of L ;
assume x in downarrow (finsups (I \/ X)) ; :: thesis: ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
then consider u being Element of L such that
A1: u >= x and
A2: u in finsups (I \/ X) by WAYBEL_0:def 15;
consider Y being finite Subset of (I \/ X) such that
A3: u = "\/" (Y,L) and
A4: ex_sup_of Y,L by A2;
Y \ X c= I

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y \ X or a in I )
assume A5: a in Y \ X ; :: thesis: a in I
then not a in X by XBOOLE_0:def 5;
hence a in I by A5, XBOOLE_0:def 3; :: thesis: verum

end;

then reconsider Z = Y \ X as finite Subset of I ;
reconsider Z9 = Z, Y9 = Y as finite Subset of L by XBOOLE_1:1;
reconsider ZX = Z9 \/ X as finite Subset of L ;

per cases ( Z = {} or Z <> {} ) ;

suppose A6: Z = {} ; :: thesis: ex i being Element of L st
( i in I & x <= i "\/" (sup X) )

A7: sup X <= i "\/" (sup X) by YELLOW_0:22;
take i ; :: thesis: ( i in I & x <= i "\/" (sup X) )
A8: ex_sup_of X,L by YELLOW_0:54;
Y c= X by A6, XBOOLE_1:37;
then u <= sup X by A3, A4, A8, YELLOW_0:34;
then u <= i "\/" (sup X) by A7, ORDERS_2:3;
hence ( i in I & x <= i "\/" (sup X) ) by A1, ORDERS_2:3; :: thesis: verum

end;

suppose A9: Z <> {} ; :: thesis: ex i being Element of L st
( i in I & x <= i "\/" (sup X) )

take sup Z9 ; :: thesis: ( sup Z9 in I & x <= (sup Z9) "\/" (sup X) )
A10: ex_sup_of X,L by YELLOW_0:54;
A11: ex_sup_of ZX,L by YELLOW_0:54;
Y c= Y \/ X by XBOOLE_1:7;
then Y c= Z9 \/ X by XBOOLE_1:39;
then A12: sup Y9 <= sup ZX by A4, A11, YELLOW_0:34;
ex_sup_of Z9,L by A9, YELLOW_0:54;
then sup (Z9 \/ X) = (sup Z9) "\/" (sup X) by A10, A11, YELLOW_0:36;
hence ( sup Z9 in I & x <= (sup Z9) "\/" (sup X) ) by A1, A3, A9, A12, ORDERS_2:3, WAYBEL_0:42; :: thesis: verum

end;

end;