let L be up-complete LATTICE; :: thesis: ( ( for X being Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ) implies for X being non empty directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) )
assume A1: for X being Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ; :: thesis: for X being non empty directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X)
let X be non empty directed Subset of L; :: thesis: for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X)
let x be Element of L; :: thesis: x "/\" (sup X) = sup ({x} "/\" X)
A2: {x} "/\" (finsups X) = { (x "/\" y) where y is Element of L : y in finsups X } by YELLOW_4:42;
reconsider T = {x} as non empty directed Subset of L by WAYBEL_0:5;
A3: ex_sup_of T "/\" X,L by WAYBEL_0:75;
A4: ex_sup_of T "/\" (finsups X),L by WAYBEL_0:75;
{x} "/\" (finsups X) is_<=_than sup ({x} "/\" X)

proof

let q be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not q in {x} "/\" (finsups X) or q <= sup ({x} "/\" X) )
assume q in {x} "/\" (finsups X) ; :: thesis: q <= sup ({x} "/\" X)
then consider y being Element of L such that
A5: ( q = x "/\" y & y in finsups X ) by A2;
consider Y being finite Subset of X such that
A6: ( y = "\/" Y,L & ex_sup_of Y,L ) by A5;
consider z being Element of L such that
A7: ( z in X & z is_>=_than Y ) by WAYBEL_0:1;
A8: "\/" Y,L <= z by A6, A7, YELLOW_0:30;
x in {x} by TARSKI:def 1;
then A9: x "/\" z <= sup ({x} "/\" X) by A3, A7, YELLOW_4:1, YELLOW_4:37;
x <= x ;
then x "/\" y <= x "/\" z by A6, A8, YELLOW_3:2;
hence q <= sup ({x} "/\" X) by A5, A9, YELLOW_0:def 2; :: thesis: verum

end;

then sup ({x} "/\" (finsups X)) <= sup ({x} "/\" X) by A4, YELLOW_0:30;
then A10: x "/\" (sup X) <= sup ({x} "/\" X) by A1;
ex_sup_of X,L by WAYBEL_0:75;
then sup ({x} "/\" X) <= x "/\" (sup X) by A3, YELLOW_4:53;
hence x "/\" (sup X) = sup ({x} "/\" X) by A10, ORDERS_2:25; :: thesis: verum