let U be Universe; :: thesis: for C being Category holds
( C is U -element iff CatToSet C is U -set )
let C be Category; :: thesis: ( C is U -element iff CatToSet C is U -set )

now :: thesis: ( C is U -element implies ( CatToSet C is Element of U & CatToSet C is U -set ) )

hereby :: thesis: verum

assume C is U -element ; :: thesis: ( CatToSet C is Element of U & CatToSet C is U -set )
then ( the carrier of C is Element of U & the carrier' of C is Element of U & 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 Th54;
hence CatToSet C is Element of U by Th13; :: thesis: CatToSet C is U -set
hence CatToSet C is U -set ; :: thesis: verum

end;

end;

hence ( C is U -element iff CatToSet C is U -set ) by Th14; :: thesis: verum