let n be Element of NAT ; for N being Subset of RelStr(# (Bags n),(DivOrder n) #) ex B being finite Subset of (Bags n) st B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #)
let N be Subset of RelStr(# (Bags n),(DivOrder n) #); ex B being finite Subset of (Bags n) st B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #)
consider B being set such that
A1:
B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #)
and
A2:
B is finite
by DICKSON:def 10;
then reconsider B = B as finite Subset of N by A2, TARSKI:def 3;
reconsider B = B as finite Subset of (Bags n) by XBOOLE_1:1;
take
B
; B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #)
thus
B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #)
by A1; verum