:: deftheorem defines FlatPoset POSET_2:def 3 :
for X being non empty set holds FlatPoset X = RelStr(# (succ X),(FlatRelat X) #);