let R be Relation; :: thesis: for a being set holds R reduces a,a
let a be set ; :: thesis: R reduces a,a
reconsider p = <*a*> as RedSequence of R by Th7;
take p ; :: according to REWRITE1:def 3 :: thesis: ( p . 1 = a & p . (len p) = a )
len p = 1 by FINSEQ_1:57;
hence ( p . 1 = a & p . (len p) = a ) by FINSEQ_1:57; :: thesis: verum