let R, S be non empty RelStr ; :: thesis: ( R is Dickson & S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S implies S \~ is well_founded )
assume that
A1: R is Dickson and
A2: S is quasi_ordered and
A3: the InternalRel of R c= the InternalRel of S and
A4: the carrier of R = the carrier of S ; :: thesis: S \~ is well_founded
S is Dickson by A1, A3, A4, Th27;
hence S \~ is well_founded by A2, Th32; :: thesis: verum