let T be TopAugmentation of R; :: thesis: T is reflexive
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
hence the InternalRel of T is_reflexive_in the carrier of T by ORDERS_2:def 2; :: according to ORDERS_2:def 2 :: thesis: verum