set F = FlatPoset X;
reconsider X = X as Element of (FlatPoset X) by LemFlatten05;
for x being Element of (FlatPoset X) holds X <= x by LemFlatten02;
hence Bottom (FlatPoset X) = X by ThMin02, LemMin01; :: thesis: verum