let n be Element of FinSETS ; :: thesis: GrothendieckUniverse n = FinSETS
FinSETS is Grothendieck of n by CLASSES3:def 4;
hence GrothendieckUniverse n = FinSETS by Th45, CLASSES3:def 5; :: thesis: verum