let L be with_suprema Poset; 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; 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; 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; ( 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))
; 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
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 A9:
Z <> {}
;
ex i being Element of L st
( i in I & x <= i "\/" (sup X) )take
sup Z9
;
( 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;
verum end; end;