0 + 1 <= n by A1, NAT_1:13;
then Seg n <> {} by FINSEQ_1:3;
hence RelStr(# (Seg n),(Nbdl1 n) #) is non empty RelStr ; :: thesis: verum