let T be TopAugmentation of R; :: thesis: T is antisymmetric
RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of R,the InternalRel of R #) by Def4;
then the InternalRel of T is_antisymmetric_in the carrier of T by ORDERS_2:def 6;
hence T is antisymmetric by ORDERS_2:def 6; :: thesis: verum