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
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 A1: A is_properly_applicable_to t ; :: thesis: T @--> reduces A ast t,t
set R = T @--> ;
consider A' being Subset of the adjectives of T such that
A2: ( A' c= A & A' is_properly_applicable_to t & A ast t = A' ast t ) and
A3: for C being Subset of the adjectives of T st C c= A' & C is_properly_applicable_to t & A ast t = C ast t holds
C = A' by A1, Th65;
consider s being one-to-one FinSequence of the adjectives of T such that
A4: ( rng s = A' & s is_properly_applicable_to t ) by A2, Th66;
reconsider p = Rev (apply s,t) as RedSequence of T @--> by A2, A3, A4, Th72;
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:65
.= s ast t by Def19
.= A ast t by A2, A4, Th57, Th58 ; :: 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:65
.= t by Def19 ; :: thesis: verum