let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; :: thesis: for t being type of T
for A being Subset of the adjectives of T st A c= adjs t holds
( A is_applicable_to t & A ast t = t )
let t be type of T; :: thesis: for A being Subset of the adjectives of T st A c= adjs t holds
( A is_applicable_to t & A ast t = t )
let a be Subset of the adjectives of T; :: thesis: ( a c= adjs t implies ( a is_applicable_to t & a ast t = t ) )
assume A1: a c= adjs t ; :: thesis: ( a is_applicable_to t & a ast t = t )
hence a is_applicable_to t by Th52; :: thesis: a ast t = t
then A2: a ast t <= t by Th49;
t <= a ast t by A1, Th52;
hence a ast t = t by A2, YELLOW_0:def 3; :: thesis: verum