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;
A3: bp in { b where b is Subset of N : b is_Dickson-basis_of N,R } by A2;
now :: thesis: for x being object st x in { b where b is Subset of N : b is_Dickson-basis_of N,R } holds
x in bool the carrier of R
let x be object ; :: 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
thus B in BB by A5; :: thesis: verum