let X be set ; :: thesis: for R being asymmetric Relation of X holds R misses id X
let R be asymmetric Relation of X; :: thesis: R misses id X
for x, y being object holds not [x,y] in R /\ (id X)

proof

let x, y be object ; :: thesis: not [x,y] in R /\ (id X)
A0: ( x in field R implies not [x,x] in R ) by RELAT_2:def 2, RELAT_2:def 10;
assume [x,y] in R /\ (id X) ; :: thesis: contradiction
then ( [x,y] in R & [x,y] in id X ) by XBOOLE_0:def 4;
hence contradiction by A0, RELAT_1:def 10, RELAT_1:15; :: thesis: verum

end;

hence R misses id X by XBOOLE_0:def 7, RELAT_1:37; :: thesis: verum