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

proof

let x, y be object ; :: thesis: not [x,y] in (R * R) /\ (id X)
assume [x,y] in (R * R) /\ (id X) ; :: thesis: contradiction
then A1: ( [x,y] in R * R & [x,y] in id X ) by XBOOLE_0:def 4;
then consider z being object such that
A2: ( [x,z] in R & [z,y] in R ) by RELAT_1:def 8;
x = y by RELAT_1:def 10, A1;
hence contradiction by LemAsym, A2; :: thesis: verum

end;

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