let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; :: thesis: for t being type of T
for a being adjective of T st a in adjs t holds
( a is_applicable_to t & a ast t = t )
let t be type of T; :: thesis: for a being adjective of T st a in adjs t holds
( a is_applicable_to t & a ast t = t )
let a be adjective of T; :: thesis: ( a in adjs t implies ( a is_applicable_to t & a ast t = t ) )
assume A1: a in adjs t ; :: thesis: ( a is_applicable_to t & a ast t = t )
hence a is_applicable_to t by Th24; :: thesis: a ast t = t
then ( t <= a ast t & a ast t <= t ) by A1, Th21, Th24;
hence a ast t = t by YELLOW_0:def 3; :: thesis: verum