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

hereby :: thesis: ( CatToSet C is U -petit implies C is U -petit )

assume C is U -petit ; :: thesis: CatToSet C is U -petit
then consider c being strict Category such that
A1: c is U -element and
A2: C ~= c ;
CatToSet c is U -set by A1, Th88;
hence CatToSet C is U -petit by Th90, A2; :: thesis: verum

end;

assume CatToSet C is U -petit ; :: thesis: C is U -petit
then consider c being CategorySet such that
A3: c is U -set and
A4: CatToSet C ~= c ;
( SetToCat c is U -element & C ~= SetToCat c ) by A4, Th87, A3, Th89;
hence C is U -petit ; :: thesis: verum