let U be Universe; :: thesis: the carrier' of (Ens U) is U -Class

A1: now :: thesis: not Maps U is U -set

assume Maps U is U -set ; :: thesis: contradiction
then proj2 (Maps U) is Element of U by CLASSES4:36;
then proj2 (Maps U) in U ;
then ( Funcs U is U -set & Funcs U is U -Class ) by Th104, Th106;
hence contradiction ; :: thesis: verum

end;

Maps U c= U by Th107;
hence the carrier' of (Ens U) is U -Class by A1; :: thesis: verum