[:X,X:] c= [:X,X:] ;
then reconsider P = [:X,X:] as Relation of X ;
R [*] c= P
proof
let x, y be object ; :: according to RELAT_1:def 3 :: 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