let IT1, IT2 be non empty Subset-Family of R; :: thesis: ( ( for B being set holds
( B in IT1 iff B is_Dickson-basis_of N,R ) ) & ( for B being set holds
( B in IT2 iff B is_Dickson-basis_of N,R ) ) implies IT1 = IT2 )
assume that
A6: for B being set holds
( B in IT1 iff B is_Dickson-basis_of N,R ) and
A7: for B being set holds
( B in IT2 iff B is_Dickson-basis_of N,R ) ; :: thesis: IT1 = IT2
for x being object holds
( x in IT1 iff x in IT2 ) by A6, A7;
hence IT1 = IT2 by TARSKI:2; :: thesis: verum