RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by Def8;
then the InternalRel of (f * N) is_antisymmetric_in the carrier of (f * N) by ORDERS_2:def 4;
hence f * N is antisymmetric ; :: thesis: verum