let X be set ; :: thesis: for R being Relation holds
( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )
let R be Relation; :: thesis: ( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )

hereby :: thesis: ( R \ (id X) is_asymmetric_in X implies R is_antisymmetric_in X )

assume A1: R is_antisymmetric_in X ; :: thesis: R \ (id X) is_asymmetric_in X
thus R \ (id X) is_asymmetric_in X :: thesis: verum

proof

let x be object ; :: according to RELAT_2:def 5 :: thesis: for y being object st x in X & y in X & [x,y] in R \ (id X) holds
not [y,x] in R \ (id X)
let y be object ; :: thesis: ( x in X & y in X & [x,y] in R \ (id X) implies not [y,x] in R \ (id X) )
assume that
A2: x in X and
A3: y in X and
A4: [x,y] in R \ (id X) ; :: thesis: not [y,x] in R \ (id X)
not [x,y] in id X by A4, XBOOLE_0:def 5;
then A5: x <> y by A2, RELAT_1:def 10;
[x,y] in R by A4, XBOOLE_0:def 5;
then not [y,x] in R by A1, A2, A3, A5;
hence not [y,x] in R \ (id X) by XBOOLE_0:def 5; :: thesis: verum

end;

end;

assume A6: R \ (id X) is_asymmetric_in X ; :: thesis: R is_antisymmetric_in X
let x be object ; :: according to RELAT_2:def 4 :: thesis: for y being object st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y
let y be object ; :: thesis: ( x in X & y in X & [x,y] in R & [y,x] in R implies x = y )
assume that
A7: ( x in X & y in X ) and
A8: [x,y] in R and
A9: [y,x] in R ; :: thesis: x = y
assume A10: x <> y ; :: thesis: contradiction
then not [y,x] in id X by RELAT_1:def 10;
then A11: [y,x] in R \ (id X) by A9, XBOOLE_0:def 5;
not [x,y] in id X by A10, RELAT_1:def 10;
then [x,y] in R \ (id X) by A8, XBOOLE_0:def 5;
hence contradiction by A6, A7, A11; :: thesis: verum