:: deftheorem defines sub ABCMIZ_0:def 23 :
for T being non empty non void TAS-structure
for a being adjective of T holds sub a = the sub-map of T . a;