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) ) )
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 & u in finsups (I \/ X) ) by WAYBEL_0:def 15;
consider Y being finite Subset of (I \/ X) such that
A2: ( u = "\/" Y,L & ex_sup_of Y,L ) by A1;
Y \ X c= I

proof

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

end;

then reconsider Z = Y \ X as finite Subset of I ;
reconsider Z' = Z, Y' = Y as finite Subset of L by XBOOLE_1:1;
reconsider ZX = Z' \/ X as finite Subset of L ;
consider i being Element of I;
reconsider i = i as Element of L ;

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

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

then ( Y c= X & ex_sup_of X,L & ex_sup_of Y',L ) by A2, XBOOLE_1:37, YELLOW_0:54;
then ( u <= sup X & sup X <= i "\/" (sup X) ) by A2, YELLOW_0:22, YELLOW_0:34;
then A3: u <= i "\/" (sup X) by ORDERS_2:26;
take i ; :: thesis: ( i in I & x <= i "\/" (sup X) )
thus ( i in I & x <= i "\/" (sup X) ) by A1, A3, ORDERS_2:26; :: thesis: verum

end;

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

then A5: ( "\/" Z,L in I & ex_sup_of Z',L & ex_sup_of X,L & ex_sup_of ZX,L ) by WAYBEL_0:42, YELLOW_0:54;
then A6: sup (Z' \/ X) = (sup Z') "\/" (sup X) by YELLOW_0:36;
Y c= Y \/ X by XBOOLE_1:7;
then Y c= Z' \/ X by XBOOLE_1:39;
then A7: sup Y' <= sup ZX by A2, A5, YELLOW_0:34;
take i = sup Z'; :: thesis: ( i in I & x <= i "\/" (sup X) )
thus ( i in I & x <= i "\/" (sup X) ) by A1, A2, A4, A6, A7, ORDERS_2:26, WAYBEL_0:42; :: thesis: verum

end;

end;