let R be RelStr ; :: thesis: ( R is empty implies R is Dickson )
assume A1: R is empty ; :: thesis: R is Dickson
now :: thesis: for N being Subset of R ex B being set st
( B is_Dickson-basis_of N,R & B is finite )
let N be Subset of R; :: thesis: ex B being set st
( B is_Dickson-basis_of N,R & B is finite )
take B = {} ; :: thesis: ( B is_Dickson-basis_of N,R & B is finite )
N = {} the carrier of R by A1;
hence B is_Dickson-basis_of N,R ; :: thesis: B is finite
thus B is finite ; :: thesis: verum
end;
hence R is Dickson ; :: thesis: verum