:: deftheorem defines TotFam TOPGEN_4:def 1 :
for T being 1-sorted holds TotFam T = bool the carrier of T;