[:X,X:] c= [:X,X:] ;
then reconsider P = [:X,X:] as Relation of X ;
R [*] c= P

proof

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 P )
let y be set ; :: thesis: ( not [x,y] in R [*] or [x,y] in P )
A1: field R c= X \/ X by RELSET_1:8;
assume A2: [x,y] in R [*] ; :: thesis: [x,y] in P
then A3: y in field R by FINSEQ_1:def 16;
x in field R by A2, FINSEQ_1:def 16;
hence [x,y] in P by A3, A1, ZFMISC_1:87; :: thesis: verum

end;

hence R [*] is Relation of X ; :: thesis: verum