let A be set ; :: thesis: for R being asymmetric Relation of A holds R misses R ~
let R be asymmetric Relation of A; :: thesis: R misses R ~
for x, y being object holds not [x,y] in R /\ (R ~)
proof
let x, y be object ; :: thesis: not [x,y] in R /\ (R ~)
assume [x,y] in R /\ (R ~) ; :: thesis: contradiction
then ( [x,y] in R & [x,y] in R ~ ) by XBOOLE_0:def 4;
then ( [x,y] in R & [y,x] in R ) by RELAT_1:def 7;
hence contradiction by LemAsym; :: thesis: verum
end;
hence R misses R ~ by RELAT_1:37, XBOOLE_0:def 7; :: thesis: verum