let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; :: thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
v ast t <= t
let t be type of T; :: thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
v ast t <= t
let v be FinSequence of the adjectives of T; :: thesis: ( v is_applicable_to t implies v ast t <= t )
assume A1: v is_applicable_to t ; :: thesis: v ast t <= t
( len (apply v,t) = (len v) + 1 & (len v) + 1 >= 1 ) by Def19, NAT_1:11;
then (len v) + 1 in dom (apply v,t) by FINSEQ_3:27;
then (apply v,t) . ((len v) + 1) in rng (apply v,t) by FUNCT_1:12;
hence v ast t <= t by A1, Th43; :: thesis: verum