[: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 )
assume [x,y] in R [*] ; :: thesis: [x,y] in P
then ( x in field R & y in field R & field R c= X \/ X & X \/ X = X ) by FINSEQ_1:def 16, RELSET_1:19;
hence [x,y] in P by ZFMISC_1:106; :: thesis: verum

end;

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