let X be non empty set ; :: thesis: for R being Relation of X holds ((R ~) `) ~ = R `
let R be Relation of X; :: thesis: ((R ~) `) ~ = R `
R = (((R ~) `) ~) ` by Tilde1;
hence ((R ~) `) ~ = R ` ; :: thesis: verum