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 t9 being type of T st t9 <= t & a in adjs t9 holds
( a is_applicable_to t & t9 <= a ast t )
let t be type of T; :: thesis: for a being adjective of T
for t9 being type of T st t9 <= t & a in adjs t9 holds
( a is_applicable_to t & t9 <= a ast t )
let a be adjective of T; :: thesis: for t9 being type of T st t9 <= t & a in adjs t9 holds
( a is_applicable_to t & t9 <= a ast t )
let t9 be type of T; :: thesis: ( t9 <= t & a in adjs t9 implies ( a is_applicable_to t & t9 <= a ast t ) )
assume that
A1: t9 <= t and
A2: a in adjs t9 ; :: thesis: ( a is_applicable_to t & t9 <= a ast t )
A3: t9 in downarrow t by A1, WAYBEL_0:17;
thus a is_applicable_to t by A1, A2, Th13; :: thesis: t9 <= a ast t
then (types a) /\ (downarrow t) is Ideal of T by Th19;
then ex_sup_of (types a) /\ (downarrow t),T by Th1;
then A4: a ast t is_>=_than (types a) /\ (downarrow t) by YELLOW_0:30;
t9 in types a by A2, Th13;
then t9 in (types a) /\ (downarrow t) by A3, XBOOLE_0:def 4;
hence t9 <= a ast t by A4; :: thesis: verum