A1: for a, b being FinSequence of D st a in {} & b in {} holds
len a = len b ;
defpred S₁[ object ] means ex Y being set st
( Y = D & Y c= D * & ( for a, b being FinSequence of D st a in Y & b in Y holds
len a = len b ) );
consider XX being set such that
A2: for x being object holds
( x in XX iff ( x in bool (D *) & S₁[x] ) ) from XBOOLE_0:sch 1();
{} c= D * ;
then reconsider A = XX as non empty set by A2, A1;
for X being set holds
( X in A iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) )

proof

let X be set ; :: thesis: ( X in A iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) )
thus ( X in A implies ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) ) :: thesis: ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) implies X in A )

proof

assume X in A ; :: thesis: ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) )
then ex Y being set st
( Y = X & Y c= D * & ( for a, b being FinSequence of D st a in Y & b in Y holds
len a = len b ) ) by A2;
hence ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) ; :: thesis: verum

end;

thus ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) implies X in A ) by A2; :: thesis: verum

end;

hence not relations_on D is empty by Def7; :: thesis: verum