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