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 Th23; :: thesis: a ast t = t
then A2: a ast t <= t by Th20;
t <= a ast t by A1, Th23;
hence a ast t = t by A2, YELLOW_0:def 3; :: thesis: verum