let X be non empty set ; :: thesis: for R being Relation of X holds R /\ ((R ~) `) is asymmetric
let R be Relation of X; :: thesis: R /\ ((R ~) `) is asymmetric
set P = R /\ ((R ~) `);
assume not R /\ ((R ~) `) is asymmetric ; :: thesis: contradiction
then consider x, y being object such that
A1: ( [x,y] in R /\ ((R ~) `) & [y,x] in R /\ ((R ~) `) ) by LemAsym;
( [x,y] in R & [x,y] in (R ~) ` ) by A1, XBOOLE_0:def 4;
then not [x,y] in R ~ by XBOOLE_0:def 5;
then not [y,x] in R by RELAT_1:def 7;
hence contradiction by A1, XBOOLE_0:def 4; :: thesis: verum