theorem Th25: :: WAYBEL16:25

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