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
for s being type of T st s in rng (apply (v,t)) holds
( v ast t <= s & s <= t )
let t be type of T; :: thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for s being type of T st s in rng (apply (v,t)) holds
( v ast t <= s & s <= t )
let v be FinSequence of the adjectives of T; :: thesis: ( v is_applicable_to t implies for s being type of T st s in rng (apply (v,t)) holds
( v ast t <= s & s <= t ) )
assume A1: v is_applicable_to t ; :: thesis: for s being type of T st s in rng (apply (v,t)) holds
( v ast t <= s & s <= t )
A2: len (apply (v,t)) = (len v) + 1 by Def19;
let s be type of T; :: thesis: ( s in rng (apply (v,t)) implies ( v ast t <= s & s <= t ) )
assume s in rng (apply (v,t)) ; :: thesis: ( v ast t <= s & s <= t )
then consider x being object such that
A3: x in dom (apply (v,t)) and
A4: s = (apply (v,t)) . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A3;
A5: x <= len (apply (v,t)) by A3, FINSEQ_3:25;
A6: (apply (v,t)) . 1 = t by Def19;
x >= 1 by A3, FINSEQ_3:25;
hence ( v ast t <= s & s <= t ) by A1, A4, A5, A2, A6, Th41; :: thesis: verum