for a, b being natural Ordinal st b <> {} holds
RED (b,a) <> {} by Th18;