let L be up-complete LATTICE; ( ( 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))
; 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; for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X)
let x be Element of L; 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
let q be
Element of
L;
LATTICE3:def 9 ( not q in {x} "/\" (finsups X) or q <= sup ({x} "/\" X) )
A5:
x <= x
;
assume
q in {x} "/\" (finsups X)
;
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;
verum
end;
ex_sup_of T "/\" (finsups X),L
by WAYBEL_0:75;
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; verum