let C1, C2 be Category; :: thesis: ( the carrier' of C1 = the carrier' of C2 & the Comp of C1 = the Comp of C2 implies C1 ~= C2 )
assume ( the carrier' of C1 = the carrier' of C2 & the Comp of C1 = the Comp of C2 ) ; :: thesis: C1 ~= C2
then alter C1 = alter C2 ;
hence C1 ~= C2 by Th50; :: thesis: verum