let T be TopAugmentation of R; :: thesis: not T is empty
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
hence not the carrier of T is empty ; :: according to STRUCT_0:def 1 :: thesis: verum