let U be Universe; :: thesis: for C being Category st C is U -element holds
( the Source of C is Element of U & the Target of C is Element of U & the Comp of C is Element of U )
let C be Category; :: thesis: ( C is U -element implies ( the Source of C is Element of U & the Target of C is Element of U & the Comp of C is Element of U ) )
assume A1: C is U -element ; :: thesis: ( the Source of C is Element of U & the Target of C is Element of U & the Comp of C is Element of U )
then reconsider cC = the carrier of C as Element of U ;
reconsider c9C = the carrier' of C as Element of U by A1;
( the Source of C c= [:c9C,cC:] & the Target of C c= [:c9C,cC:] & the Comp of C c= [:[:c9C,c9C:],c9C:] ) ;
hence ( the Source of C is Element of U & the Target of C is Element of U & the Comp of C is Element of U ) by CLASSES4:13; :: thesis: verum