let x, y be object ; :: thesis: for R being Relation st <*x,y*> is RedSequence of R holds
[x,y] in R
let R be Relation; :: thesis: ( <*x,y*> is RedSequence of R implies [x,y] in R )
set P = <*x,y*>;
A1: ( <*x,y*> . 1 = x & <*x,y*> . 2 = y ) ;
len <*x,y*> = 2 by FINSEQ_1:44;
then ( 1 in dom <*x,y*> & 1 + 1 in dom <*x,y*> ) by FINSEQ_3:25;
hence ( <*x,y*> is RedSequence of R implies [x,y] in R ) by A1, REWRITE1:def 2; :: thesis: verum