Transitive reduction should occur before root at universal in bundle closure. Rooting at universal preserves reduction; in principle it's simpler this way.
Code for OWL Class Expression of a Difference duplicated code from Intersection. It's cleaner to convert to Intersection first and then convert.
Two minor tweaks: