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 ;
then A5: x <> y by ;
[x,y] in R by ;
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:
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 ;
not [x,y] in id X by ;
then [x,y] in R \ (id X) by ;
hence contradiction by A6, A7, A11; :: thesis: verum