for L being non empty Poset
for X being Subset of L st X is order-generating holds
Irr L c= X