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