let R be Relation; :: thesis: R c= R [*]
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R or [x,y] in R [*] )
A1: len <*x,y*> = 2 by FINSEQ_1:44;
A2: <*x,y*> . 2 = y ;
assume A3: [x,y] in R ; :: thesis: [x,y] in R [*]
then A4: y in field R by RELAT_1:15;
A5: <*x,y*> . 1 = x ;

A6: now :: thesis: for i being Nat st i >= 1 & i < 2 holds
[(<*x,y*> . i),(<*x,y*> . (i + 1))] in R

let i be Nat; :: thesis: ( i >= 1 & i < 2 implies [(<*x,y*> . i),(<*x,y*> . (i + 1))] in R )
assume that
A7: i >= 1 and
A8: i < 2 ; :: thesis: [(<*x,y*> . i),(<*x,y*> . (i + 1))] in R
1 + 1 = 2 ;
then i <= 1 by A8, NAT_1:13;
then i = 1 by A7, XXREAL_0:1;
hence [(<*x,y*> . i),(<*x,y*> . (i + 1))] in R by A3; :: thesis: verum

end;

x in field R by A3, RELAT_1:15;
hence [x,y] in R [*] by A4, A1, A5, A2, A6, FINSEQ_1:def 17; :: thesis: verum