theorem :: ORDINAL1:30

for Z being set holds {} is Sequence of Z