let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; :: thesis: for t being type of T
for A being finite Subset of the adjectives of T st A is_properly_applicable_to t holds
T @--> reduces A ast t,t
set R = T @--> ;
let t be type of T; :: thesis: for A being finite Subset of the adjectives of T st A is_properly_applicable_to t holds
T @--> reduces A ast t,t
let A be finite Subset of the adjectives of T; :: thesis: ( A is_properly_applicable_to t implies T @--> reduces A ast t,t )
assume A is_properly_applicable_to t ; :: thesis: T @--> reduces A ast t,t
then consider A9 being Subset of the adjectives of T such that
A9 c= A and
A1: A9 is_properly_applicable_to t and
A2: A ast t = A9 ast t and
A3: for C being Subset of the adjectives of T st C c= A9 & C is_properly_applicable_to t & A ast t = C ast t holds
C = A9 by Th64;
consider s being one-to-one FinSequence of the adjectives of T such that
A4: rng s = A9 and
A5: s is_properly_applicable_to t by A1, Th65;
reconsider p = Rev (apply (s,t)) as RedSequence of T @--> by A2, A3, A4, A5, Th71;
take p ; :: according to REWRITE1:def 3 :: thesis: ( p . 1 = A ast t & p . (len p) = t )
thus p . 1 = (apply (s,t)) . (len (apply (s,t))) by FINSEQ_5:62
.= s ast t by Def19
.= A ast t by A2, A4, A5, Th56, Th57 ; :: thesis: p . (len p) = t
thus p . (len p) = p . (len (apply (s,t))) by FINSEQ_5:def 3
.= (apply (s,t)) . 1 by FINSEQ_5:62
.= t by Def19 ; :: thesis: verum