let A, B be set ; :: thesis: for R being Relation of A,B holds (R `) ~ = (R ~) `
let R be Relation of A,B; :: thesis: (R `) ~ = (R ~) `
(R `) ~ = ([:A,B:] ~) \ (R ~) by RELAT_1:24
.= (R ~) ` by SYSREL:5 ;
hence (R `) ~ = (R ~) ` ; :: thesis: verum