theorem :: WAYBEL34:47

for W being with_non-empty_element set holds W -INF(SC)_category = Intersect ((W -INF_category),(W -UPS_category))