defpred S₁[ set ] means ex Y being set st
( Y = $1 & Y c= D * & ( for a, b being FinSequence of D st a in Y & b in Y holds
len a = len b ) );
consider A being set such that
A1: for x being set holds
( x in A iff ( x in bool (D *) & S₁[x] ) ) from XBOOLE_0:sch 1();
take A ; :: thesis: 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 ) ) )
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 A1;
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 A1; :: thesis: verum

end;

hence 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 ) ) ) ; :: thesis: verum