theorem :: DICKSON:25

for R being RelStr holds {} is_Dickson-basis_of {} the carrier of R,R ;