set IR = the InternalRel of R;
set IR9 = the InternalRel of (R \~);
set CR9 = the carrier of (R \~);
now :: thesis: for x, y being object st 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 \~) holds
x = y
let x, y be object ; :: 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 \~) ;
hence R \~ is antisymmetric ; :: thesis: verum