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 [*] )
assume A1: [x,y] in R ; :: thesis: [x,y] in R [*]
then A2: ( x in field R & y in field R ) by RELAT_1:30;
A3: ( len <*x,y*> = 2 & 2 >= 1 & <*x,y*> . 1 = x & <*x,y*> . 2 = y ) by FINSEQ_1:61;

now

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

end;

hence [x,y] in R [*] by A2, A3, FINSEQ_1:def 16; :: thesis: verum