:: deftheorem defines FlatRelat POSET_2:def 2 :
for X being non empty set holds FlatRelat X = ({[X,X]} \/ [:{X},X:]) \/ (id X);