set IR = the InternalRel of R;
set IR9 = the InternalRel of (R \~ );
set CR9 = 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 \~ ) and
y in the carrier of (R \~ ) and
A1: [x,y] in the InternalRel of (R \~ ) and
A2: [y,x] in the InternalRel of (R \~ ) ; :: thesis: x = y
not [x,y] in the InternalRel of R ~ by A1, XBOOLE_0:def 5;
hence x = y by A2, 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