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