let L be up-complete Semilattice; :: thesis: ( ( for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ) implies for D being non empty directed Subset of L
for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D) )
assume A1: for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ; :: thesis: for D being non empty directed Subset of L
for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D)
let D be non empty directed Subset of L; :: thesis: for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D)
let x be Element of L; :: thesis: x "/\" (sup D) = sup ({x} "/\" D)
ex w being Element of L st
( x >= w & sup D >= w & ( for c being Element of L st x >= c & sup D >= c holds
w >= c ) ) by LATTICE3:def 11;
then x "/\" (sup D) <= sup D by LATTICE3:def 14;
then A2: x "/\" (sup D) <= sup ({(x "/\" (sup D))} "/\" D) by A1;
reconsider T = {(x "/\" (sup D))} as non empty directed Subset of L by WAYBEL_0:5;
ex_sup_of D,L by WAYBEL_0:75;
then A3: sup D is_>=_than D by YELLOW_0:30;
( ex_sup_of T "/\" D,L & {(x "/\" (sup D))} "/\" D is_<=_than x "/\" (sup D) ) by WAYBEL_0:75, YELLOW_4:52;
then sup ({(x "/\" (sup D))} "/\" D) <= x "/\" (sup D) by YELLOW_0:30;
hence x "/\" (sup D) = sup ({(x "/\" (sup D))} "/\" D) by A2, ORDERS_2:2
.= sup (({x} "/\" {(sup D)}) "/\" D) by YELLOW_4:46
.= sup ({x} "/\" ({(sup D)} "/\" D)) by YELLOW_4:41
.= sup ({x} "/\" D) by A3, YELLOW_4:51 ;
:: thesis: verum