theorem :: JORDAN1B:1

for f being FinSequence holds
( f is empty iff Rev f is empty )