:: deftheorem defines meet-continuous WAYBEL_2:def 7 :
for R being non empty reflexive RelStr holds
( R is meet-continuous iff ( R is up-complete & R is satisfying_MC ) );