:: deftheorem defines is_properly_applicable_to ABCMIZ_0:def 27 :
for T being non empty non void TAS-structure
for t being Element of T
for a being adjective of T holds
( a is_properly_applicable_to t iff ( t <= sub a & a is_applicable_to t ) );