let X be set ; for R being Relation st R is_asymmetric_in X holds
R \/ (id X) is_antisymmetric_in X
let R be Relation; ( R is_asymmetric_in X implies R \/ (id X) is_antisymmetric_in X )
assume A1:
R is_asymmetric_in X
; R \/ (id X) is_antisymmetric_in X
let x be object ; RELAT_2:def 4 for y being object st x in X & y in X & [x,y] in R \/ (id X) & [y,x] in R \/ (id X) holds
x = y
let y be object ; ( x in X & y in X & [x,y] in R \/ (id X) & [y,x] in R \/ (id X) implies x = y )
assume that
A2:
( x in X & y in X )
and
A3:
[x,y] in R \/ (id X)
and
A4:
[y,x] in R \/ (id X)
; x = y
assume A5:
x <> y
; contradiction
then
not [y,x] in id X
by RELAT_1:def 10;
then A6:
[y,x] in R
by A4, XBOOLE_0:def 3;
not [x,y] in id X
by A5, RELAT_1:def 10;
then
[x,y] in R
by A3, XBOOLE_0:def 3;
hence
contradiction
by A1, A2, A6; verum