set IR = the InternalRel of R;
set IR' = the InternalRel of (R \~ );
set CR' = the carrier of (R \~ );

now

let x, y be set ; :: thesis: ( x in the carrier of (R \~ ) & y in the carrier of (R \~ ) & [x,y] in the InternalRel of (R \~ ) & [y,x] in the InternalRel of (R \~ ) implies x = y )
assume that
( x in the carrier of (R \~ ) & y in the carrier of (R \~ ) ) and
A1: ( [x,y] in the InternalRel of (R \~ ) & [y,x] in the InternalRel of (R \~ ) ) ; :: thesis: x = y
( not [x,y] in the InternalRel of R ~ & [y,x] in the InternalRel of R ) by A1, XBOOLE_0:def 5;
hence x = y by RELAT_1:def 7; :: thesis: verum

end;

then the InternalRel of (R \~ ) is_antisymmetric_in the carrier of (R \~ ) by RELAT_2:def 4;
hence R \~ is antisymmetric by ORDERS_2:def 6; :: thesis: verum