let R be non empty RelStr ; :: thesis: for N being non empty Subset of R
for B being set st B is_Dickson-basis_of N,R holds
not B is empty
let N be non empty Subset of R; :: thesis: for B being set st B is_Dickson-basis_of N,R holds
not B is empty
let B be set ; :: thesis: ( B is_Dickson-basis_of N,R implies not B is empty )
assume A1: B is_Dickson-basis_of N,R ; :: thesis: not B is empty
consider a being Element of N;
consider b being Element of R such that
A2: ( b in B & b <= a ) by A1, Def9;
thus not B is empty by A2; :: thesis: verum