let R be Relation; :: thesis: R c= R [*]
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in R or [x,b₁] in R [*] )
let y be set ; :: thesis: ( not [x,y] in R or [x,y] in R [*] )
A1: len <*x,y*> = 2 by FINSEQ_1:61;
A2: <*x,y*> . 2 = y by FINSEQ_1:61;
assume A3: [x,y] in R ; :: thesis: [x,y] in R [*]
then A4: y in field R by RELAT_1:30;
A5: <*x,y*> . 1 = x by FINSEQ_1:61;

A6: now

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, A5, FINSEQ_1:61; :: thesis: verum

end;

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