let A be set ; :: thesis: for R being asymmetric Relation of A holds R \/ (id A) is antisymmetric
let R be asymmetric Relation of A; :: thesis: R \/ (id A) is antisymmetric
for x, y being object st [x,y] in R \/ (id A) & [y,x] in R \/ (id A) holds
x = y

proof

let x, y be object ; :: thesis: ( [x,y] in R \/ (id A) & [y,x] in R \/ (id A) implies x = y )
assume A1: ( [x,y] in R \/ (id A) & [y,x] in R \/ (id A) ) ; :: thesis: x = y
then Z0: ( [x,y] in R or [x,y] in id A ) by XBOOLE_0:def 3;
Z1: ( [y,x] in R or [y,x] in id A ) by XBOOLE_0:def 3, A1;
assume x <> y ; :: thesis: contradiction
hence contradiction by Z1, RELAT_1:def 10, LemAsym, Z0; :: thesis: verum

end;

hence R \/ (id A) is antisymmetric by LemAntisym; :: thesis: verum