theorem Th69: :: CLASSES5:67

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