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(# {{} },(id {{} }) #) by YELLOW_1:26;
set pp = product p;
set cpp = the carrier of (product p);
set ipp = the InternalRel of (product p);
A2: the InternalRel of (product p) = id {{} } by YELLOW_1:26;
thus not product p is empty by YELLOW_1:26; :: thesis: ( product p is quasi_ordered & product p is Dickson & product p is antisymmetric )
thus product p is quasi_ordered :: thesis: ( product p is Dickson & product p is antisymmetric )

proof

thus product p is reflexive by YELLOW_1:26; :: according to DICKSON:def 3 :: thesis: product p is transitive
let x, y, z be set ; :: according to RELAT_2:def 8,ORDERS_2:def 5 :: thesis: ( not x in the carrier of (product p) or not y in the carrier of (product p) or not z in the carrier of (product p) or not [x,y] in the InternalRel of (product p) or not [y,z] in the InternalRel of (product p) or [x,z] in the InternalRel of (product p) )
assume ( x in the carrier of (product p) & y in the carrier of (product p) & z in the carrier of (product p) & [x,y] in the InternalRel of (product p) & [y,z] in the InternalRel of (product p) ) ; :: thesis: [x,z] in the InternalRel of (product p)
hence [x,z] in the InternalRel of (product p) by A2, RELAT_1:def 10; :: thesis: verum

end;

thus product p is Dickson :: thesis: product p is antisymmetric

proof

let N be Subset of the carrier of (product p); :: 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 A1, ZFMISC_1:39;

suppose A3: 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 )
N = {} the carrier of (product p) by A3;
hence B is_Dickson-basis_of N, product p by Th26; :: thesis: B is finite
thus B is finite ; :: thesis: verum

end;

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 (product p) st a in N holds
ex b being Element of (product p) st
( b in B & b <= a )
let a be Element of (product p); :: thesis: ( a in N implies ex b being Element of (product p) st
( b in B & b <= a ) )
assume A5: a in N ; :: thesis: ex b being Element of (product p) 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 A4, A5, RELAT_1:def 10;
hence b <= a by A2, ORDERS_2:def 9; :: thesis: verum

end;

thus B is finite ; :: thesis: verum

end;

end;

end;

thus product p is antisymmetric by YELLOW_1:26; :: thesis: verum