let P be TolStr ; :: thesis: ( P is empty implies TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr )
assume P is empty ; :: thesis: TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr
then the carrier of P = {} ;
hence TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr ; :: thesis: verum