(Flatten f) . (Bottom (FlatPoset X)) = Bottom (FlatPoset Y) by DefFlatten04;
hence Flatten f is continuous by Thflat07; :: thesis: verum