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
A2: (len v) + 1 >= 1 by NAT_1:11;
len (apply (v,t)) = (len v) + 1 by Def19;
then (len v) + 1 in dom (apply (v,t)) by A2, FINSEQ_3:25;
then (apply (v,t)) . ((len v) + 1) in rng (apply (v,t)) by FUNCT_1:3;
hence v ast t <= t by A1, Th42; :: thesis: verum