let X be set ; :: thesis: for R being Relation st id X c= R holds
id X c= R ~
let R be Relation; :: thesis: ( id X c= R implies id X c= R ~ )
assume A1: id X c= R ; :: thesis: id X c= R ~
for x being object st x in X holds
[x,x] in R ~

proof

let x be object ; :: thesis: ( x in X implies [x,x] in R ~ )
assume x in X ; :: thesis: [x,x] in R ~
then [x,x] in id X by RELAT_1:def 10;
hence [x,x] in R ~ by A1, RELAT_1:def 7; :: thesis: verum

end;

hence id X c= R ~ by RELAT_1:47; :: thesis: verum