let R be RelStr ; :: thesis: ( R is empty implies R is Dickson )
assume A1: R is empty ; :: thesis: R is Dickson
A2: the carrier of R is empty by A1;

now

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 A2;
hence B is_Dickson-basis_of N,R by Th26; :: thesis: B is finite
thus B is finite ; :: thesis: verum

end;

hence R is Dickson by Def10; :: thesis: verum