let R be NatRelStr of 0 ; :: thesis: R is empty
the carrier of R = 0 by Def7;
hence R is empty ; :: thesis: verum