set BB = { b where b is Subset of N : b is_Dickson-basis_of N,R } ;
set CR = the carrier of R;
consider bp being set such that
A2: bp is_Dickson-basis_of N,R and
bp is finite by A1, Def10;
bp c= N by A2, Def9;
then A3: bp in { b where b is Subset of N : b is_Dickson-basis_of N,R } by A2;

now

let x be set ; :: thesis: ( x in { b where b is Subset of N : b is_Dickson-basis_of N,R } implies x in bool the carrier of R )
assume x in { b where b is Subset of N : b is_Dickson-basis_of N,R } ; :: thesis: x in bool the carrier of R
then consider b being Subset of N such that
A4: x = b and
b is_Dickson-basis_of N,R ;
b c= the carrier of R by XBOOLE_1:1;
hence x in bool the carrier of R by A4; :: thesis: verum

end;

then reconsider BB = { b where b is Subset of N : b is_Dickson-basis_of N,R } as non empty Subset-Family of the carrier of R by A3, TARSKI:def 3;
take BB ; :: thesis: for B being set holds
( B in BB iff B is_Dickson-basis_of N,R )
let B be set ; :: thesis: ( B in BB iff B is_Dickson-basis_of N,R )

hereby :: thesis: ( B is_Dickson-basis_of N,R implies B in BB )

assume B in BB ; :: thesis: B is_Dickson-basis_of N,R
then ex b being Subset of N st
( b = B & b is_Dickson-basis_of N,R ) ;
hence B is_Dickson-basis_of N,R ; :: thesis: verum

end;

assume A5: B is_Dickson-basis_of N,R ; :: thesis: B in BB
then B c= N by Def9;
hence B in BB by A5; :: thesis: verum