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:41
.= (R ~ ) ` by SYSREL:18 ;
hence (R ` ) ~ = (R ~ ) ` ; :: thesis: verum