let n be Element of NAT ; :: thesis: 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) #); :: thesis: 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;
now :: thesis: for u being object st u in B holds
u in N
let u be object ; :: thesis: ( u in B implies u in N )
assume A3: u in B ; :: thesis: u in N
B c= N by A1, DICKSON:def 9;
hence u in N by A3; :: thesis: verum
end;
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 ; :: thesis: 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; :: thesis: verum