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