:: deftheorem defines FinPoset BAGORDER:def 16 :
for R being non empty connected Poset holds FinPoset R = RelStr(# (Fin the carrier of R),(FinOrd R) #);