let T be non empty reflexive transitive antisymmetric TA-structure ; :: thesis: for t being type of T holds ({} the adjectives of T) ast t = t
let t be type of T; :: thesis: ({} the adjectives of T) ast t = t
set A = {} the adjectives of T;
types ({} the adjectives of T) = the carrier of T by Th16;
then (types ({} the adjectives of T)) /\ (downarrow t) = downarrow t by XBOOLE_1:28;
hence ({} the adjectives of T) ast t = t by WAYBEL_0:34; :: thesis: verum