let r1, r2 be Element of relations_on D; :: thesis: ( ( for a being FinSequence of D holds not a in r1 ) & ( for a being FinSequence of D holds not a in r2 ) implies r1 = r2 )
assume that
A3: for a being FinSequence of D holds not a in r1 and
A4: for a being FinSequence of D holds not a in r2 ; :: thesis: r1 = r2
for a being FinSequence of D holds
( a in r1 iff a in r2 ) by A3, A4;
hence r1 = r2 by Def9; :: thesis: verum