:: deftheorem defines smooth ABCMIZ_1:def 53 :
for L being non empty Poset holds
( L is smooth iff ex C being initialized ConstructorSignature ex f being Function of L,VarPoset st
( the carrier of L c= QuasiTypes C & f = (vars-function C) | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) ) );