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

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

thus
product p is antisymmetric
by YELLOW_1:26; :: thesis: verum
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 )

end;( B is_Dickson-basis_of N, product p & B is finite )

per cases
( N = {} or N = {{}} )
by A1, ZFMISC_1:33;

end;

suppose A3:
N = {}
; :: thesis: ex B being set st

( B is_Dickson-basis_of N, product p & B is finite )

( 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 ; :: thesis: B is finite

thus B is finite ; :: thesis: verum

end;N = {} the carrier of (product p) by A3;

hence B is_Dickson-basis_of N, product p ; :: thesis: B is finite

thus B is finite ; :: thesis: verum

suppose A4:
N = {{}}
; :: thesis: ex B being set st

( B is_Dickson-basis_of N, product p & B is finite )

( 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

end;thus B is_Dickson-basis_of N, product p :: thesis: B is finite

proof

thus
B is finite
; :: thesis: verum
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;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