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

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