let R be non empty RelStr ; :: thesis:
assume A1: R is quasi_ordered ; :: thesis:
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~);

hereby :: thesis:

assume that
A2: R is connected and
A3: R \~ is well_founded ; :: thesis:
let N be non empty Subset of the carrier of R; :: thesis:
consider x being object such that
A4: x in min-classes N by A3, Th19;
consider a being Element of (R \~) such that
A5: a is_minimal_wrt N, the InternalRel of (R \~) and
A6: x = (Class ((EqRel R),a)) /\ N by A4, Def8;
A7: a in N by A5, WAYBEL_4:def 25;

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in min-classes N ; :: thesis:
then consider b being Element of (R \~) such that
A8: b is_minimal_wrt N, the InternalRel of (R \~) and
A9: y = (Class ((EqRel R),b)) /\ N by Def8;
A10: b in N by A8, WAYBEL_4:def 25;
reconsider a9 = a as Element of R ;
reconsider b9 = b as Element of R ;

A11: now :: thesis:

per cases by A2, WAYBEL_0:def 29;

suppose A12: a9 <= b9 ; :: thesis:

then A13: [a,b] in the InternalRel of R ;

now :: thesis:

per cases ;

suppose a = b ; :: thesis:

hence [b,a] in the InternalRel of R by A12; :: thesis:

end;

suppose A14: a <> b ; :: thesis:

now :: thesis:

assume not [b,a] in the InternalRel of R ; :: thesis:
then not [a,b] in the InternalRel of R ~ by RELAT_1:def 7;
then [a,b] in the InternalRel of R \ ( the InternalRel of R ~) by A13, XBOOLE_0:def 5;
hence contradiction by A7, A8, A14, WAYBEL_4:def 25; :: thesis:

end;

hence [b,a] in the InternalRel of R ; :: thesis:

end;

end;

end;

hence ( [a,b] in the InternalRel of R & [b,a] in the InternalRel of R ) by A12; :: thesis:

end;

suppose A15: b9 <= a9 ; :: thesis:

then A16: [b,a] in the InternalRel of R ;

now :: thesis:

per cases ;

suppose a = b ; :: thesis:

hence [a,b] in the InternalRel of R by A15; :: thesis:

end;

suppose A17: a <> b ; :: thesis:

now :: thesis:

assume not [a,b] in the InternalRel of R ; :: thesis:
then not [b,a] in the InternalRel of R ~ by RELAT_1:def 7;
then [b,a] in the InternalRel of R \ ( the InternalRel of R ~) by A16, XBOOLE_0:def 5;
hence contradiction by A5, A10, A17, WAYBEL_4:def 25; :: thesis:

end;

hence [a,b] in the InternalRel of R ; :: thesis:

end;

end;

end;

hence ( [a,b] in the InternalRel of R & [b,a] in the InternalRel of R ) by A15; :: thesis:

end;

end;

end;

then [b,a] in the InternalRel of R ~ by RELAT_1:def 7;
then [b,a] in the InternalRel of R /\ ( the InternalRel of R ~) by A11, XBOOLE_0:def 4;
then [b,a] in EqRel R by A1, Def4;
then b in Class ((EqRel R),a) by EQREL_1:19;
then Class ((EqRel R),b) = Class ((EqRel R),a) by EQREL_1:23;
hence y in {x} by A6, A9, TARSKI:def 1; :: thesis:

end;

assume y in {x} ; :: thesis:
then y = (Class ((EqRel R),a)) /\ N by A6, TARSKI:def 1;
hence y in min-classes N by A5, Def8; :: thesis:

end;

then min-classes N = {x} by TARSKI:2;
hence card (min-classes N) = 1 by CARD_1:30; :: thesis:

end;

assume A18: for N being non empty Subset of R holds card (min-classes N) = 1 ; :: thesis:

now :: thesis:

let a, b be Element of R; :: thesis:
assume that
A19: not a <= b and
A20: not a >= b ; :: thesis:
A21: not [a,b] in the InternalRel of R by A19;
then A22: not [b,a] in the InternalRel of R ~ by RELAT_1:def 7;
not [b,a] in the InternalRel of R by A20;
then A23: not [a,b] in the InternalRel of R ~ by RELAT_1:def 7;
set N9 = {a,b};
set MCN = {{a},{b}};

now :: thesis:

let x be object ; :: thesis:
reconsider xx = x as set by TARSKI:1;

hereby :: thesis:

assume x in min-classes {a,b} ; :: thesis:
then consider y being Element of (R \~) such that
A24: y is_minimal_wrt {a,b}, the InternalRel of (R \~) and
A25: x = (Class ((EqRel R),y)) /\ {a,b} by Def8;
A26: y in {a,b} by A24, WAYBEL_4:def 25;

per cases by A26, TARSKI:def 2;

suppose A27: y = a ; :: thesis:

now :: thesis:

let z be object ; :: thesis:

hereby :: thesis:

assume A28: z in xx ; :: thesis:
then A29: z in Class ((EqRel R),a) by A25, A27, XBOOLE_0:def 4;
A30: z in {a,b} by A25, A28, XBOOLE_0:def 4;

now :: thesis:

per cases by A30, TARSKI:def 2;

suppose z = a ; :: thesis:

hence z in {a} by TARSKI:def 1; :: thesis:

end;

suppose z = b ; :: thesis:

then [b,a] in EqRel R by A29, EQREL_1:19;
then [b,a] in the InternalRel of R /\ ( the InternalRel of R ~) by A1, Def4;
hence z in {a} by A22, XBOOLE_0:def 4; :: thesis:

end;

end;

end;

hence z in {a} ; :: thesis:

end;

assume z in {a} ; :: thesis:
then A31: z = a by TARSKI:def 1;
then A32: z in {a,b} by TARSKI:def 2;
z in Class ((EqRel R),a) by A31, EQREL_1:20;
hence z in xx by A25, A27, A32, XBOOLE_0:def 4; :: thesis:

end;

then x = {a} by TARSKI:2;
hence x in {{a},{b}} by TARSKI:def 2; :: thesis:

end;

suppose A33: y = b ; :: thesis:

now :: thesis:

let z be object ; :: thesis:

hereby :: thesis:

assume A34: z in xx ; :: thesis:
then A35: z in Class ((EqRel R),b) by A25, A33, XBOOLE_0:def 4;
A36: z in {a,b} by A25, A34, XBOOLE_0:def 4;

now :: thesis:

per cases by A36, TARSKI:def 2;

suppose z = b ; :: thesis:

hence z in {b} by TARSKI:def 1; :: thesis:

end;

suppose z = a ; :: thesis:

then [a,b] in EqRel R by A35, EQREL_1:19;
then [a,b] in the InternalRel of R /\ ( the InternalRel of R ~) by A1, Def4;
hence z in {b} by A21, XBOOLE_0:def 4; :: thesis:

end;

end;

end;

hence z in {b} ; :: thesis:

end;

assume z in {b} ; :: thesis:
then A37: z = b by TARSKI:def 1;
then A38: z in {a,b} by TARSKI:def 2;
z in Class ((EqRel R),b) by A37, EQREL_1:20;
hence z in xx by A25, A33, A38, XBOOLE_0:def 4; :: thesis:

end;

then x = {b} by TARSKI:2;
hence x in {{a},{b}} by TARSKI:def 2; :: thesis:

end;

end;

end;

assume A39: x in {{a},{b}} ; :: thesis:

per cases by A39, TARSKI:def 2;

suppose A40: x = {a} ; :: thesis:

now :: thesis:

reconsider a9 = a as Element of (R \~) ;
take a9 = a9; :: thesis:
A41: a9 in {a,b} by TARSKI:def 2;

now :: thesis:

assume ex y being set st
( y in {a,b} & y <> a9 & [y,a9] in the InternalRel of (R \~) ) ; :: thesis:
then consider y being set such that
A42: y in {a,b} and
A43: y <> a9 and
A44: [y,a9] in the InternalRel of (R \~) ;
y = b by A42, A43, TARSKI:def 2;
hence contradiction by A20, A44; :: thesis:

end;

hence a9 is_minimal_wrt {a,b}, the InternalRel of (R \~) by A41, WAYBEL_4:def 25; :: thesis:

now :: thesis:

let z be object ; :: thesis:

hereby :: thesis:

assume z in xx ; :: thesis:
then A45: z = a by A40, TARSKI:def 1;
then z in Class ((EqRel R),a) by EQREL_1:20;
hence z in (Class ((EqRel R),a)) /\ {a,b} by A41, A45, XBOOLE_0:def 4; :: thesis:

end;

assume A46: z in (Class ((EqRel R),a)) /\ {a,b} ; :: thesis:
then A47: z in Class ((EqRel R),a) by XBOOLE_0:def 4;
A48: z in {a,b} by A46, XBOOLE_0:def 4;

per cases by A48, TARSKI:def 2;

suppose z = a ; :: thesis:

hence z in xx by A40, TARSKI:def 1; :: thesis:

end;

suppose z = b ; :: thesis:

then [b,a] in EqRel R by A47, EQREL_1:19;
then [b,a] in the InternalRel of R /\ ( the InternalRel of R ~) by A1, Def4;
hence z in xx by A22, XBOOLE_0:def 4; :: thesis:

end;

end;

end;

hence x = (Class ((EqRel R),a9)) /\ {a,b} by TARSKI:2; :: thesis:

end;

hence x in min-classes {a,b} by Def8; :: thesis:

end;

suppose A49: x = {b} ; :: thesis:

now :: thesis:

reconsider b9 = b as Element of (R \~) ;
take b9 = b9; :: thesis:
A50: b9 in {a,b} by TARSKI:def 2;

now :: thesis:

assume ex y being set st
( y in {a,b} & y <> b9 & [y,b9] in the InternalRel of (R \~) ) ; :: thesis:
then consider y being set such that
A51: y in {a,b} and
A52: y <> b9 and
A53: [y,b9] in the InternalRel of (R \~) ;
y = a by A51, A52, TARSKI:def 2;
hence contradiction by A19, A53; :: thesis:

end;

hence b9 is_minimal_wrt {a,b}, the InternalRel of (R \~) by A50, WAYBEL_4:def 25; :: thesis:

now :: thesis:

let z be object ; :: thesis:

hereby :: thesis:

assume z in xx ; :: thesis:
then A54: z = b by A49, TARSKI:def 1;
then z in Class ((EqRel R),b) by EQREL_1:20;
hence z in (Class ((EqRel R),b)) /\ {a,b} by A50, A54, XBOOLE_0:def 4; :: thesis:

end;

assume A55: z in (Class ((EqRel R),b)) /\ {a,b} ; :: thesis:
then A56: z in Class ((EqRel R),b) by XBOOLE_0:def 4;
A57: z in {a,b} by A55, XBOOLE_0:def 4;

per cases by A57, TARSKI:def 2;

suppose z = b ; :: thesis:

hence z in xx by A49, TARSKI:def 1; :: thesis:

end;

suppose z = a ; :: thesis:

then [a,b] in EqRel R by A56, EQREL_1:19;
then [a,b] in the InternalRel of R /\ ( the InternalRel of R ~) by A1, Def4;
hence z in xx by A23, XBOOLE_0:def 4; :: thesis:

end;

end;

end;

hence x = (Class ((EqRel R),b9)) /\ {a,b} by TARSKI:2; :: thesis:

end;

hence x in min-classes {a,b} by Def8; :: thesis:

end;

end;

end;

then min-classes {a,b} = {{a},{b}} by TARSKI:2;
then A58: card {{a},{b}} = 1 by A18;

now :: thesis:

assume {a} = {b} ; :: thesis:
then A59: a = b by ZFMISC_1:3;
R is reflexive by A1;
then the InternalRel of R is_reflexive_in the carrier of R ;
hence contradiction by A21, A59; :: thesis:

end;

hence contradiction by A58, CARD_2:57; :: thesis:

end;

hence R is connected by WAYBEL_0:def 29; :: thesis:

now :: thesis:

let N be Subset of R; :: thesis:
assume N <> {} ; :: thesis:
then card (min-classes N) = 1 by A18;
then min-classes N <> {} ;
hence ex x being object st x in min-classes N by XBOOLE_0:def 1; :: thesis:

end;

hence R \~ is well_founded by Th19; :: thesis: