let X be set ; :: thesis:
let R be Relation of X; :: thesis:

per cases ;

suppose A1: not X is empty ; :: thesis:

hereby :: thesis:

assume R is antisymmetric ; :: thesis:
then R is_antisymmetric_in X by A1, PARTIT_2:24;
hence R \ (id X) is asymmetric by A1, RELAT_2:3, PARTIT_2:29; :: thesis:

end;

assume R \ (id X) is asymmetric ; :: thesis:
then R \ (id X) is_asymmetric_in X by A1, PARTIT_2:28;
hence R is antisymmetric by A1, RELAT_2:3, PARTIT_2:25; :: thesis:

end;

suppose X is empty ; :: thesis:

hence ( R is antisymmetric iff R \ (id X) is asymmetric ) ; :: thesis:

end;

end;