theorem LemFlatten05: :: POSET_2:13

for X being non empty set holds X is Element of (FlatPoset X)