let X be set ; :: thesis: for R being Relation of X holds R /\ (R ~) is symmetric
let R be Relation of X; :: thesis: R /\ (R ~) is symmetric
(R /\ (R ~)) ~ = (R ~) /\ ((R ~) ~) by RELAT_1:22
.= (R ~) /\ R ;
hence R /\ (R ~) is symmetric by RELAT_2:13; :: thesis: verum