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 ex x being set st x in p by XBOOLE_0:def 1;
hence contradiction by A1; :: thesis: verum