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 )
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 set such that
A2: ( x in dom (apply v,t) & s = (apply v,t) . x ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A2;
A3: ( 1 <= 1 & x >= 1 & x <= len (apply v,t) & (len v) + 1 <= (len v) + 1 ) by A2, FINSEQ_3:27;
( len (apply v,t) = (len v) + 1 & (apply v,t) . 1 = t & v ast t = (apply v,t) . ((len v) + 1) ) by Def19;
hence ( v ast t <= s & s <= t ) by A1, A2, A3, Th42; :: thesis: verum