:: deftheorem Def31 defines @--> ABCMIZ_0:def 31 :
for T being non empty reflexive transitive non void TAS-structure
for b₂ being Relation of T holds
( b₂ = T @--> iff for t1, t2 being type of T holds
( [t1,t2] in b₂ iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) );