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

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

suppose A6: Z = {} ; :: thesis: ex i being Element of 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:26;
hence ( i in I & x <= i "\/" (sup X) ) by A1, ORDERS_2:26; :: thesis: verum

end;

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

take i = sup Z'; :: thesis: ( i in I & x <= i "\/" (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= Z' \/ X by XBOOLE_1:39;
then A12: sup Y' <= sup ZX by A4, A11, YELLOW_0:34;
ex_sup_of Z',L by A9, YELLOW_0:54;
then sup (Z' \/ X) = (sup Z') "\/" (sup X) by A10, A11, YELLOW_0:36;
hence ( i in I & x <= i "\/" (sup X) ) by A1, A3, A9, A12, ORDERS_2:26, WAYBEL_0:42; :: thesis: verum

end;

end;