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 )
thus ( R is_antisymmetric_in X implies R \ (id X) is_asymmetric_in X ) :: thesis: ( R \ (id X) is_asymmetric_in X implies R is_antisymmetric_in X )

proof

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

now

let x, y be set ; :: 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, Def4;
hence not [y,x] in R \ (id X) by XBOOLE_0:def 5; :: thesis: verum

end;

hence R \ (id X) is_asymmetric_in X by Def5; :: thesis: verum

end;

thus ( R \ (id X) is_asymmetric_in X implies R is_antisymmetric_in X ) :: thesis: verum

proof

assume A6: R \ (id X) is_asymmetric_in X ; :: thesis: R is_antisymmetric_in X

now

let x, y be set ; :: 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

now

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, Def5; :: thesis: verum

end;

hence x = y ; :: thesis: verum

end;

hence R is_antisymmetric_in X by Def4; :: thesis: verum

end;