for M being RelStr st M is Dickson & M is quasi_ordered holds
( [:M,OrderedNAT:] is quasi_ordered & [:M,OrderedNAT:] is Dickson ) by Th36;