let R be Relation; :: thesis: for a, b being object st [a,b] in R holds
R reduces a,b
let a, b be object ; :: thesis: ( [a,b] in R implies R reduces a,b )
assume [a,b] in R ; :: thesis: R reduces a,b
then reconsider p = <*a,b*> as RedSequence of R by Th7;
take p ; :: according to REWRITE1:def 3 :: thesis: ( p . 1 = a & p . (len p) = b )
len p = 2 by FINSEQ_1:44;
hence ( p . 1 = a & p . (len p) = b ) by FINSEQ_1:44; :: thesis: verum