theorem :: CLASSES5:91
for U being Universe
for C, D being CategorySet st C is U -set & D is U -set holds
Functors (C,D) is U -set