theorem Th68: :: CLASSES5:66

for C, D being Category holds Funct (C,D) c= bool [: the carrier' of C, the carrier' of D:]