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
for t' being type of T st t' <= t & a in adjs t' holds
( a is_applicable_to t & t' <= a ast t )
let t be type of T; :: thesis: for a being adjective of T
for t' being type of T st t' <= t & a in adjs t' holds
( a is_applicable_to t & t' <= a ast t )
let a be adjective of T; :: thesis: for t' being type of T st t' <= t & a in adjs t' holds
( a is_applicable_to t & t' <= a ast t )
let t' be type of T; :: thesis: ( t' <= t & a in adjs t' implies ( a is_applicable_to t & t' <= a ast t ) )
assume A1: ( t' <= t & a in adjs t' ) ; :: thesis: ( a is_applicable_to t & t' <= a ast t )
then A2: ( t' in downarrow t & t' in types a ) by Th13, WAYBEL_0:17;
thus a is_applicable_to t :: thesis: t' <= a ast t

proof

take t' ; :: according to ABCMIZ_0:def 15 :: thesis: ( t' in types a & t' <= t )
thus ( t' in types a & t' <= t ) by A1, Th13; :: thesis: verum

end;

then (types a) /\ (downarrow t) is Ideal of T by Th20;
then ( ex_sup_of (types a) /\ (downarrow t),T & a ast t = sup ((types a) /\ (downarrow t)) ) by Th1;
then ( a ast t is_>=_than (types a) /\ (downarrow t) & t' in (types a) /\ (downarrow t) ) by A2, XBOOLE_0:def 4, YELLOW_0:30;
hence t' <= a ast t by LATTICE3:def 9; :: thesis: verum