let L be up-complete LATTICE; :: thesis: ( L is meet-continuous iff for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D) )

thus ( L is meet-continuous implies for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D) ) by Th45; :: thesis: ( ( for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D) ) implies L is meet-continuous )

assume for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D) ; :: thesis: L is meet-continuous

then for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x <= sup ({x} "/\" D) ;

then inf_op L is directed-sups-preserving by Th46;

then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43;

hence L is meet-continuous by Th51; :: thesis: verum

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D) )

thus ( L is meet-continuous implies for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D) ) by Th45; :: thesis: ( ( for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D) ) implies L is meet-continuous )

assume for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D) ; :: thesis: L is meet-continuous

then for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x <= sup ({x} "/\" D) ;

then inf_op L is directed-sups-preserving by Th46;

then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43;

hence L is meet-continuous by Th51; :: thesis: verum