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
set a = the Element of N;
ex b being Element of R st
( b in B & b <= the Element of N ) by A1;
hence not B is empty ; :: thesis: verum