theorem :: CLASSES4:92

for X being set
for S being Sequence st S = sequence_univers X holds
( last S = {} & S . NAT = {} )