:: deftheorem defines OrderedFIN CARDFIL3:def 2 :
for I being set holds OrderedFIN I = InclPoset (Fin I);