let R be non empty Poset; for N being non empty Subset of R st R is Dickson holds
ex B being set st
( B is_Dickson-basis_of N,R & ( for C being set st C is_Dickson-basis_of N,R holds
B c= C ) )
let N be non empty Subset of R; ( R is Dickson implies ex B being set st
( B is_Dickson-basis_of N,R & ( for C being set st C is_Dickson-basis_of N,R holds
B c= C ) ) )
assume A1:
R is Dickson
; ex B being set st
( B is_Dickson-basis_of N,R & ( for C being set st C is_Dickson-basis_of N,R holds
B c= C ) )
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~);
set B = { b where b is Element of (R \~) : b is_minimal_wrt N, the InternalRel of (R \~) } ;
A2:
R is quasi_ordered
;
for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j )
by A1, Th28;
then
not min-classes N is empty
by A2, Th30;
then consider x being object such that
A3:
x in min-classes N
by XBOOLE_0:def 1;
consider y being Element of (R \~) such that
A4:
y is_minimal_wrt N, the InternalRel of (R \~)
and
x = (Class ((EqRel R),y)) /\ N
by A3, Def8;
y in { b where b is Element of (R \~) : b is_minimal_wrt N, the InternalRel of (R \~) }
by A4;
then reconsider B = { b where b is Element of (R \~) : b is_minimal_wrt N, the InternalRel of (R \~) } as non empty set ;
take
B
; ( B is_Dickson-basis_of N,R & ( for C being set st C is_Dickson-basis_of N,R holds
B c= C ) )
then A6:
B c= N
;
thus
B is_Dickson-basis_of N,R
for C being set st C is_Dickson-basis_of N,R holds
B c= Cproof
thus
B c= N
by A5;
DICKSON:def 9 for a being Element of R st a in N holds
ex b being Element of R st
( b in B & b <= a )
let a be
Element of
R;
( a in N implies ex b being Element of R st
( b in B & b <= a ) )
assume A7:
a in N
;
ex b being Element of R st
( b in B & b <= a )
reconsider a9 =
a as
Element of
(R \~) ;
now ex b being Element of R st
( b in B & b <= a )assume A8:
for
b being
Element of
R holds
( not
b in B or not
b <= a )
;
contradictionper cases
( ( the InternalRel of (R \~) -Seg a) /\ N = {} or ( the InternalRel of (R \~) -Seg a) /\ N <> {} )
;
suppose A9:
( the InternalRel of (R \~) -Seg a) /\ N <> {}
;
contradiction
R \~ is
well_founded
by A1, A2, Th32;
then
the
InternalRel of
(R \~) is_well_founded_in the
carrier of
R
by WELLFND1:def 2;
then consider z being
object such that A10:
z in ( the InternalRel of (R \~) -Seg a) /\ N
and A11:
the
InternalRel of
(R \~) -Seg z misses ( the InternalRel of (R \~) -Seg a) /\ N
by A9, WELLORD1:def 3;
A12:
z in the
InternalRel of
(R \~) -Seg a
by A10, XBOOLE_0:def 4;
then
[z,a] in the
InternalRel of
(R \~)
by WELLORD1:1;
then
z in dom the
InternalRel of
(R \~)
by XTUPLE_0:def 12;
then reconsider z =
z as
Element of
(R \~) ;
reconsider z9 =
z as
Element of
R ;
z is_minimal_wrt ( the InternalRel of (R \~) -Seg a9) /\ N, the
InternalRel of
(R \~)
by A10, A11, Th5;
then
z is_minimal_wrt N, the
InternalRel of
(R \~)
by Th6;
then A13:
z in B
;
[z,a] in the
InternalRel of
R \ ( the InternalRel of R ~)
by A12, WELLORD1:1;
then
z9 <= a
;
hence
contradiction
by A8, A13;
verum end; end;
hence
ex
b being
Element of
R st
(
b in B &
b <= a )
;
verum
end;
let C be set ; ( C is_Dickson-basis_of N,R implies B c= C )
assume A14:
C is_Dickson-basis_of N,R
; B c= C
A15:
C c= N
by A14;
now for b being object st b in B holds
b in Clet b be
object ;
( b in B implies b in C )assume A16:
b in B
;
b in C
b in N
by A5, A16;
then reconsider b9 =
b as
Element of
R ;
consider c being
Element of
R such that A17:
c in C
and A18:
c <= b9
by A6, A14, A16;
A19:
ex
b99 being
Element of
(R \~) st
(
b99 = b &
b99 is_minimal_wrt N, the
InternalRel of
(R \~) )
by A16;
A20:
[c,b] in the
InternalRel of
R
by A18;
A21:
the
InternalRel of
R is_antisymmetric_in the
carrier of
R
by ORDERS_2:def 4;
[b,c] in the
InternalRel of
R
by A15, A17, A19, A20, Th16;
hence
b in C
by A17, A18, A21;
verum end;
hence
B c= C
; verum