let p be RelStr-yielding ManySortedSet of {} ; :: thesis: ( not product p is empty & product p is quasi_ordered & product p is Dickson & product p is antisymmetric )
A1: product p = RelStr(# ,() #) by YELLOW_1:26;
set pp = product p;
set cpp = the carrier of ();
set ipp = the InternalRel of ();
A2: the InternalRel of () = id by YELLOW_1:26;
thus not product p is empty by YELLOW_1:26; :: thesis:
thus product p is quasi_ordered by YELLOW_1:26; :: thesis: ( product p is Dickson & product p is antisymmetric )
thus product p is Dickson :: thesis:
proof
let N be Subset of the carrier of (); :: according to DICKSON:def 10 :: thesis: ex B being set st
( B is_Dickson-basis_of N, product p & B is finite )

per cases ( N = {} or N = ) by ;
suppose A4: N = ; :: thesis: ex B being set st
( B is_Dickson-basis_of N, product p & B is finite )

take B = ; :: thesis: ( B is_Dickson-basis_of N, product p & B is finite )
thus B is_Dickson-basis_of N, product p :: thesis: B is finite
proof
thus B c= N by A4; :: according to DICKSON:def 9 :: thesis: for a being Element of () st a in N holds
ex b being Element of () st
( b in B & b <= a )

let a be Element of (); :: thesis: ( a in N implies ex b being Element of () st
( b in B & b <= a ) )

assume A5: a in N ; :: thesis: ex b being Element of () st
( b in B & b <= a )

take b = a; :: thesis: ( b in B & b <= a )
thus b in B by A4, A5; :: thesis: b <= a
[b,a] in id by ;
hence b <= a by A2; :: thesis: verum
end;
thus B is finite ; :: thesis: verum
end;
end;
end;
thus product p is antisymmetric by YELLOW_1:26; :: thesis: verum