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