:: deftheorem defines min_func POSET_1:def 11 :
for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) = P --> (Bottom Q);