let C, D be strict Category; :: thesis: ( C ~= D implies CatToSet C ~= CatToSet D )
assume A1: C ~= D ; :: thesis: CatToSet C ~= CatToSet D
( C = SetToCat (CatToSet C) & D = SetToCat (CatToSet D) ) by Th87;
hence CatToSet C ~= CatToSet D by A1; :: thesis: verum