let R be RelStr ; :: thesis: {} is_Dickson-basis_of {} the carrier of R,R
set N = {} the carrier of R;
thus {} c= {} the carrier of R ; :: according to DICKSON:def 9 :: thesis: for a being Element of R st a in {} the carrier of R holds
ex b being Element of R st
( b in {} & b <= a )
thus for a being Element of R st a in {} the carrier of R holds
ex b being Element of R st
( b in {} & b <= a ) ; :: thesis: verum