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
let x be set ; :: according to RELAT_2:def 4 :: thesis: for y being set 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 set ; :: thesis: ( 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) ; :: thesis: x = y
assume A5: x <> y ; :: thesis: 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, Def5; :: thesis: verum