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

now

let x be set ; :: thesis: ( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )

hereby :: thesis: ( x in IT2 implies x in IT1 )

assume x in IT1 ; :: thesis: x in IT2
then x is_Dickson-basis_of N,R by A6;
hence x in IT2 by A7; :: thesis: verum

end;

assume x in IT2 ; :: thesis: x in IT1
then x is_Dickson-basis_of N,R by A7;
hence x in IT1 by A6; :: thesis: verum

end;

hence IT1 = IT2 by TARSKI:1; :: thesis: verum