let R be non empty RelStr ; :: thesis: ( R is quasi_ordered & R is Dickson implies R \~ is well_founded )
assume that
A1: R is quasi_ordered and
A2: R is Dickson ; :: thesis: R \~ is well_founded
A3: for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j ) by A2, Th28;
now :: thesis: for N being Subset of R st N <> {} holds
ex x being object st x in min-classes N
let N be Subset of R; :: thesis: ( N <> {} implies ex x being object st x in min-classes N )
assume N <> {} ; :: thesis: ex x being object st x in min-classes N
then not min-classes N is empty by A1, A3, Th30;
hence ex x being object st x in min-classes N by XBOOLE_0:def 1; :: thesis: verum
end;
hence R \~ is well_founded by Th19; :: thesis: verum