let P be RelStr ; :: thesis: ( P is empty implies P is discrete )
assume A1: P is empty ; :: thesis: P is discrete
then A2: the carrier of P = {} ;
the InternalRel of P = {} by A1;
hence P is discrete by A2, Def1, RELAT_1:81; :: thesis: verum