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)

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} "/\" (finsups X) = { (x "/\" y) where y is Element of L : y in finsups X } by YELLOW_4:42;

A4: {x} "/\" (finsups X) is_<=_than sup ({x} "/\" X)

then sup ({x} "/\" (finsups X)) <= sup ({x} "/\" X) by A4, YELLOW_0:30;

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 A2, YELLOW_4:53;

hence x "/\" (sup X) = sup ({x} "/\" X) by A13, ORDERS_2:2; :: thesis: verum

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)

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} "/\" (finsups X) = { (x "/\" y) where y is Element of L : y in finsups X } by YELLOW_4:42;

A4: {x} "/\" (finsups X) is_<=_than sup ({x} "/\" X)

proof

ex_sup_of T "/\" (finsups X),L
by WAYBEL_0:75;
let q be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not q in {x} "/\" (finsups X) or q <= sup ({x} "/\" X) )

A5: x <= x ;

assume q in {x} "/\" (finsups 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 A9, A11, YELLOW_0:30;

then A12: x "/\" y <= x "/\" z by A8, A5, YELLOW_3:2;

x in {x} by TARSKI:def 1;

then x "/\" z <= sup ({x} "/\" X) by A2, A10, YELLOW_4:1, YELLOW_4:37;

hence q <= sup ({x} "/\" X) by A6, A12, YELLOW_0:def 2; :: thesis: verum

end;A5: x <= x ;

assume q in {x} "/\" (finsups 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 A9, A11, YELLOW_0:30;

then A12: x "/\" y <= x "/\" z by A8, A5, YELLOW_3:2;

x in {x} by TARSKI:def 1;

then x "/\" z <= sup ({x} "/\" X) by A2, A10, YELLOW_4:1, YELLOW_4:37;

hence q <= sup ({x} "/\" X) by A6, A12, YELLOW_0:def 2; :: thesis: verum

then sup ({x} "/\" (finsups X)) <= sup ({x} "/\" X) by A4, YELLOW_0:30;

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 A2, YELLOW_4:53;

hence x "/\" (sup X) = sup ({x} "/\" X) by A13, ORDERS_2:2; :: thesis: verum