for X being non empty set
for x, y being Element of (FlatPoset X) holds
( x <= y iff ( x = X or x = y ) ) by LemFlatten01, LemFlatten02;