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 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 st A is_properly_applicable_to t holds
T @--> reduces A ast t,t
let A be finite Subset of ; :: 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 A' being Subset of such that
A' c= A and
A1: A' is_properly_applicable_to t and
A2: A ast t = A' ast t and
A3: for C being Subset of st C c= A' & C is_properly_applicable_to t & A ast t = C ast t holds
C = A' by Th65;
consider s being one-to-one FinSequence of the adjectives of T such that
A4: rng s = A' and
A5: s is_properly_applicable_to t by A1, Th66;
reconsider p = Rev (apply s,t) as RedSequence of T @--> by A2, A3, A4, A5, 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, A5, 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