let R be non empty RelStr ; :: thesis:
assume that
A1: R is quasi_ordered and
A2: for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j ) ; :: thesis:
set IR = the InternalRel of R;
set IR9 = the InternalRel of (R \~);
A3: R is transitive by A1;
let N be non empty Subset of R; :: thesis:
assume A4: ( not min-classes N is finite or min-classes N is empty ) ; :: thesis:

per cases by A4;

suppose A5: min-classes N is infinite ; :: thesis:

then reconsider MCN = min-classes N as infinite set ;
consider f being sequence of (min-classes N) such that
A6: f is one-to-one by A5, Th2;
deffunc H₁( object ) -> Element of f . $1 = the Element of f . $1;

A7: now :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider x9 = x as Element of NAT ;
f . x9 is Element of min-classes N ;
then A8: f . x in MCN ;
then not f . x is empty by Th21;
then the Element of f . x9 in f . x ;
hence H₁(x) in the carrier of R by A8; :: thesis:

end;

consider g being sequence of the carrier of R such that
A9: for x being object st x in NAT holds
g . x = H₁(x) from FUNCT_2:sch 2(A7);
reconsider g = g as sequence of R ;
consider i, j being Nat such that
A10: i < j and
A11: g . i <= g . j by A2;
reconsider gi = g . i, gj = g . j as Element of (R \~) ;
A12: [gi,gj] in the InternalRel of R by A11;
A13: f . i in MCN ;
then A14: not f . i is empty by Th21;
A15: f . j in MCN ;
then A16: not f . j is empty by Th21;
j in NAT by ORDINAL1:def 12;
then A17: g . j = the Element of f . j by A9;
i in NAT by ORDINAL1:def 12;
then A18: g . i = the Element of f . i by A9;
A19: gj is_minimal_wrt N, the InternalRel of (R \~) by A1, A15, A16, A17, Th18;
gi is_minimal_wrt N, the InternalRel of (R \~) by A1, A13, A14, A18, Th18;
then A20: gi in N by WAYBEL_4:def 25;

A21: now :: thesis:

per cases ;

suppose gi = gj ; :: thesis:

hence [gi,gj] in the InternalRel of R ~ by A12, RELAT_1:def 7; :: thesis:

end;

suppose A22: gi <> gj ; :: thesis:

now :: thesis:

assume not [gi,gj] in the InternalRel of R ~ ; :: thesis:
then [gi,gj] in the InternalRel of R \ ( the InternalRel of R ~) by A12, XBOOLE_0:def 5;
hence contradiction by A19, A20, A22, WAYBEL_4:def 25; :: thesis:

end;

hence [gi,gj] in the InternalRel of R ~ ; :: thesis:

end;

[gi,gj] in the InternalRel of R by A11;
then [gi,gj] in the InternalRel of R /\ ( the InternalRel of R ~) by A21, XBOOLE_0:def 4;
then [gi,gj] in EqRel R by A1, Def4;
then gi in Class ((EqRel R),gj) by EQREL_1:19;
then A23: Class ((EqRel R),gj) = Class ((EqRel R),gi) by EQREL_1:23;
consider mj being Element of (R \~) such that
mj is_minimal_wrt N, the InternalRel of (R \~) and
A24: f . j = (Class ((EqRel R),mj)) /\ N by A15, Def8;
consider mi being Element of (R \~) such that
mi is_minimal_wrt N, the InternalRel of (R \~) and
A25: f . i = (Class ((EqRel R),mi)) /\ N by A13, Def8;
gj in Class ((EqRel R),mj) by A16, A17, A24, XBOOLE_0:def 4;
then A26: Class ((EqRel R),gj) = Class ((EqRel R),mj) by EQREL_1:23;
A27: i in NAT by ORDINAL1:def 12;
A28: j in NAT by ORDINAL1:def 12;
gi in Class ((EqRel R),mi) by A14, A18, A25, XBOOLE_0:def 4;
then f . i = f . j by A23, A24, A25, A26, EQREL_1:23;
hence contradiction by A5, A6, A10, FUNCT_2:19, A27, A28; :: thesis:

end;

suppose A29: min-classes N is empty ; :: thesis:

deffunc H₁( set , set ) -> Element of (( the InternalRel of R -Seg $2) /\ N) \ (Class ((EqRel R),$2)) = the Element of (( the InternalRel of R -Seg $2) /\ N) \ (Class ((EqRel R),$2));
consider f being Function such that
A30: dom f = NAT and
A31: f . 0 = the Element of N and
A32: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 11();
defpred S₁[ Nat] means f . $1 in N;
A33: S₁[ 0 ] by A31;

A34: now :: thesis:

let i be Nat; :: thesis:
assume A35: S₁[i] ; :: thesis:
reconsider fi = f . i as Element of (R \~) by A35;
set IC = (( the InternalRel of R -Seg fi) /\ N) \ (Class ((EqRel R),fi));
A36: f . (i + 1) = the Element of (( the InternalRel of R -Seg (f . i)) /\ N) \ (Class ((EqRel R),(f . i))) by A32;

now :: thesis:

assume (( the InternalRel of R -Seg fi) /\ N) \ (Class ((EqRel R),fi)) is empty ; :: thesis:
then ( the InternalRel of R -Seg fi) /\ N c= Class ((EqRel R),fi) by XBOOLE_1:37;
hence contradiction by A1, A29, A35, Th20, Th29; :: thesis:

end;

then f . (i + 1) in ( the InternalRel of R -Seg (f . i)) /\ N by A36, XBOOLE_0:def 5;
hence S₁[i + 1] by XBOOLE_0:def 4; :: thesis:

end;

A37: for i being Nat holds S₁[i] from NAT_1:sch 2(A33, A34);

now :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then f . x in N by A37;
hence f . x in the carrier of R ; :: thesis:

end;

then reconsider f = f as sequence of R by A30, FUNCT_2:3;

A38: now :: thesis:

let i be Nat; :: thesis:
defpred S₂[ Nat] means ( i < $1 implies f . i >= f . $1 );
A39: S₂[ 0 ] by NAT_1:2;
A40: for j being Nat st S₂[j] holds
S₂[j + 1]

proof

let j be Nat; :: thesis:
assume that
A41: ( i < j implies f . i >= f . j ) and
A42: i < j + 1 ; :: thesis:
A43: i <= j by A42, NAT_1:13;
reconsider fj = f . j, fj1 = f . (j + 1) as Element of (R \~) ;
set IC = (( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj));
A44: fj in N by A37;
A45: fj1 = the Element of (( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj)) by A32;

now :: thesis:

assume (( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj)) is empty ; :: thesis:
then ( the InternalRel of R -Seg fj) /\ N c= Class ((EqRel R),fj) by XBOOLE_1:37;
hence contradiction by A1, A29, A44, Th20, Th29; :: thesis:

end;

then fj1 in ( the InternalRel of R -Seg fj) /\ N by A45, XBOOLE_0:def 5;
then fj1 in the InternalRel of R -Seg fj by XBOOLE_0:def 4;
then A46: [fj1,fj] in the InternalRel of R by WELLORD1:1;
then A47: f . j >= f . (j + 1) ;

per cases by A43, XXREAL_0:1;

suppose i < j ; :: thesis:

hence f . i >= f . (j + 1) by A3, A41, A47, ORDERS_2:3; :: thesis:

end;

suppose i = j ; :: thesis:

hence f . i >= f . (j + 1) by A46; :: thesis:

end;

thus for j being Nat holds S₂[j] from NAT_1:sch 2(A39, A40); :: thesis:

end;

now :: thesis:

let i be Nat; :: thesis:
defpred S₂[ Nat] means ( i < $1 implies not f . i <= f . $1 );
A48: S₂[ 0 ] by NAT_1:2;
A49: for j being Nat st S₂[j] holds
S₂[j + 1]

proof

let j be Nat; :: thesis:
assume that
( i < j implies not f . i <= f . j ) and
A50: i < j + 1 ; :: thesis:
A51: i <= j by A50, NAT_1:13;
reconsider fj = f . j, fj1 = f . (j + 1) as Element of (R \~) ;
A52: fj in N by A37;

per cases by A51, XXREAL_0:1;

suppose A53: i < j ; :: thesis:

assume A54: f . i <= f . (j + 1) ; :: thesis:
j < j + 1 by NAT_1:13;
then A55: f . j >= f . (j + 1) by A38;
f . i >= f . j by A38, A53;
then f . j <= f . (j + 1) by A3, A54, ORDERS_2:3;
then A56: fj1 in Class ((EqRel R),fj) by A1, A55, Th7;
set IC = (( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj));
A57: fj1 = the Element of (( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj)) by A32;

now :: thesis:

end;

hence contradiction by A56, A57, XBOOLE_0:def 5; :: thesis:

end;

suppose A58: i = j ; :: thesis:

assume A59: f . i <= f . (j + 1) ; :: thesis:
j < j + 1 by NAT_1:13;
then f . (j + 1) <= f . j by A38;
then A60: fj1 in Class ((EqRel R),fj) by A1, A58, A59, Th7;
set IC = (( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj));
A61: fj1 = the Element of (( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj)) by A32;

now :: thesis:

end;

hence contradiction by A60, A61, XBOOLE_0:def 5; :: thesis:

end;

thus for j being Nat holds S₂[j] from NAT_1:sch 2(A48, A49); :: thesis:

end;

hence contradiction by A2; :: thesis:

end;