let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; :: thesis: for t being type of T
for A being Subset of the adjectives of T st A is_applicable_to t holds
A c= adjs (A ast t)
let t be type of T; :: thesis: for A being Subset of the adjectives of T st A is_applicable_to t holds
A c= adjs (A ast t)
let a be Subset of the adjectives of T; :: thesis: ( a is_applicable_to t implies a c= adjs (a ast t) )
assume a is_applicable_to t ; :: thesis: a c= adjs (a ast t)
then (types a) /\ (downarrow t) is Ideal of T by Th26;
then sup ((types a) /\ (downarrow t)) in (types a) /\ (downarrow t) by Th1;
then a ast t in types a by XBOOLE_0:def 4;
hence a c= adjs (a ast t) by Th14; :: thesis: verum