:: deftheorem defines ConstOSSet OSALG_1:def 15 :
for R being non empty Poset
for z being non empty set holds ConstOSSet (R,z) = the carrier of R --> z;