let x, y be set ; :: 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 ) by FINSEQ_1:61;
len <*x,y*> = 2 by FINSEQ_1:61;
then A2: ( 1 in dom <*x,y*> & 1 + 1 in dom <*x,y*> ) by FINSEQ_3:27;
assume <*x,y*> is RedSequence of R ; :: thesis: [x,y] in R
hence [x,y] in R by A1, A2, REWRITE1:def 2; :: thesis: verum