let U be Universe; :: thesis: ( Ens U is non U -small Category & the carrier of (Ens U) is U -Class & the carrier' of (Ens U) is U -Class )
A1: not the carrier of (Ens U) in U ;
then not Ens U is U -element ;
hence Ens U is non U -small Category ; :: thesis: ( the carrier of (Ens U) is U -Class & the carrier' of (Ens U) is U -Class )
the carrier of (Ens U) c= U ;
hence the carrier of (Ens U) is U -Class by A1; :: thesis: the carrier' of (Ens U) is U -Class
thus the carrier' of (Ens U) is U -Class by Th108; :: thesis: verum