let p be relation; :: thesis: ( ( for a being FinSequence holds not a in p ) implies p = {} )
assume A1: for a being FinSequence holds not a in p ; :: thesis: p = {}
assume p <> {} ; :: thesis: contradiction
then consider x being set such that
A2: x in p by XBOOLE_0:def 1;
x is FinSequence by A2, Def1;
hence contradiction by A1, A2; :: thesis: verum