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 by YELLOW_1:26; :: thesis: ( product p is Dickson & product p is antisymmetric )
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:33;
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; :: thesis: verum
end;
thus B is finite ; :: thesis: verum
end;
end;
end;
thus product p is antisymmetric by YELLOW_1:26; :: thesis: verum