let R be Relation; :: thesis: for a, b being set st [a,b] in R holds
<*a,b*> is RedSequence of R
let a, b be set ; :: thesis: ( [a,b] in R implies <*a,b*> is RedSequence of R )
assume A1: [a,b] in R ; :: thesis: <*a,b*> is RedSequence of R
set p = <*a,b*>;
A2: ( len <*a,b*> = 1 + 1 & dom <*a,b*> = Seg (len <*a,b*>) ) by FINSEQ_1:61, FINSEQ_1:def 3;
thus len <*a,b*> > 0 by FINSEQ_1:61; :: according to REWRITE1:def 2 :: thesis: for i being Element of NAT st i in dom <*a,b*> & i + 1 in dom <*a,b*> holds
[(<*a,b*> . i),(<*a,b*> . (i + 1))] in R
A3: ( <*a,b*> . 1 = a & <*a,b*> . (len <*a,b*>) = b ) by A2, FINSEQ_1:61;
let i be Element of NAT ; :: thesis: ( i in dom <*a,b*> & i + 1 in dom <*a,b*> implies [(<*a,b*> . i),(<*a,b*> . (i + 1))] in R )
assume ( i in dom <*a,b*> & i + 1 in dom <*a,b*> ) ; :: thesis: [(<*a,b*> . i),(<*a,b*> . (i + 1))] in R
then ( i >= 1 & i + 1 <= 1 + 1 ) by A2, Lm1;
then ( i <= 1 & i >= 1 ) by XREAL_1:8;
then i = 1 by XXREAL_0:1;
hence [(<*a,b*> . i),(<*a,b*> . (i + 1))] in R by A1, A3, FINSEQ_1:61; :: thesis: verum