let X be set ; :: thesis: for R being Relation of X holds
( R is antisymmetric iff R \ (id X) is asymmetric )
let R be Relation of X; :: thesis: ( R is antisymmetric iff R \ (id X) is asymmetric )

per cases ( not X is empty or X is empty ) ;

suppose A1: not X is empty ; :: thesis: ( R is antisymmetric iff R \ (id X) is asymmetric )

hereby :: thesis: ( R \ (id X) is asymmetric implies R is antisymmetric )

assume R is antisymmetric ; :: thesis: R \ (id X) is asymmetric
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: verum

end;

assume R \ (id X) is asymmetric ; :: thesis: R is antisymmetric
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: verum

end;

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

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

end;

end;