let L be up-complete LATTICE; :: thesis: ( L is meet-continuous iff for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) )
hereby :: thesis: ( ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) implies L is meet-continuous )
assume L is meet-continuous ; :: thesis: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
then ( SupMap L is meet-preserving & SupMap L is join-preserving ) ;
hence for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) by Th38; :: thesis: verum
end;
assume for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ; :: thesis: L is meet-continuous
then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40;
hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def 7 :: thesis: verum