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 is_applicable_to t holds
a ast t <= t
let t be type of T; :: thesis: for a being adjective of T st a is_applicable_to t holds
a ast t <= t
let a be adjective of T; :: thesis: ( a is_applicable_to t implies a ast t <= t )
assume a is_applicable_to t ; :: thesis: a ast t <= t
then (types a) /\ (downarrow t) is Ideal of T by Th19;
then sup ((types a) /\ (downarrow t)) in (types a) /\ (downarrow t) by Th1;
then a ast t in downarrow t by XBOOLE_0:def 4;
hence a ast t <= t by WAYBEL_0:17; :: thesis: verum