let X be set ; :: thesis: for R being Relation st R is_asymmetric_in X holds
R \/ (id X) is_antisymmetric_in X
let R be Relation; :: thesis: ( R is_asymmetric_in X implies R \/ (id X) is_antisymmetric_in X )
assume A1: R is_asymmetric_in X ; :: thesis: R \/ (id X) is_antisymmetric_in X

now

let x, y be set ; :: thesis: ( x in X & y in X & [x,y] in R \/ (id X) & [y,x] in R \/ (id X) implies x = y )
assume A2: ( x in X & y in X & [x,y] in R \/ (id X) & [y,x] in R \/ (id X) ) ; :: thesis: x = y

now

assume x <> y ; :: thesis: contradiction
then ( not [x,y] in id X & not [y,x] in id X ) by RELAT_1:def 10;
then ( [x,y] in R & [y,x] in R ) by A2, XBOOLE_0:def 3;
hence contradiction by A1, A2, Def5; :: thesis: verum

end;

hence x = y ; :: thesis: verum

end;

hence R \/ (id X) is_antisymmetric_in X by Def4; :: thesis: verum