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} "/\" ()) ) 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} "/\" ()) ; :: 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)
reconsider T = {x} as non empty directed Subset of L by WAYBEL_0:5;
A2: ex_sup_of T "/\" X,L by WAYBEL_0:75;
A3: {x} "/\" () = { (x "/\" y) where y is Element of L : y in finsups X } by YELLOW_4:42;
A4: {x} "/\" () is_<=_than sup ({x} "/\" X)
proof
let q be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not q in {x} "/\" () or q <= sup ({x} "/\" X) )
A5: x <= x ;
assume q in {x} "/\" () ; :: thesis: q <= sup ({x} "/\" X)
then consider y being Element of L such that
A6: q = x "/\" y and
A7: y in finsups X by A3;
consider Y being finite Subset of X such that
A8: y = "\/" (Y,L) and
A9: ex_sup_of Y,L by A7;
consider z being Element of L such that
A10: z in X and
A11: z is_>=_than Y by WAYBEL_0:1;
"\/" (Y,L) <= z by ;
then A12: x "/\" y <= x "/\" z by ;
x in {x} by TARSKI:def 1;
then x "/\" z <= sup ({x} "/\" X) by ;
hence q <= sup ({x} "/\" X) by ; :: thesis: verum
end;
ex_sup_of T "/\" (),L by WAYBEL_0:75;
then sup ({x} "/\" ()) <= sup ({x} "/\" X) by ;
then A13: 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 ;
hence x "/\" (sup X) = sup ({x} "/\" X) by ; :: thesis: verum