Logical order is different from genetic order in mathematics. Bourbaki chose logical order. Genetic order is so much more pleasant and informative - but this is only my personal view. This also gets reflected in the way people choose how to organize their mathematical ideas in proof assistants. There is *no single way* which is better than all other ways. However, let me say that I love the genetic way much better than the logical way. It is just the way my brain happens to work. Of course, people are allowed to have their own personal views of the "graph of mathematical ideas" (Is this a so-called "subtweet"?)