Theorem Order.isIdeal_sUnion_of_directedOn

Modification history