let R be non empty RelStr ; :: thesis: ( R is quasi_ordered implies ( ( R is connected & R \~ is well_founded ) iff for N being non empty Subset of R holds card (min-classes N) = 1 ) )
assume A1: R is quasi_ordered ; :: thesis: ( ( R is connected & R \~ is well_founded ) iff for N being non empty Subset of R holds card (min-classes N) = 1 )
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~);

hereby :: thesis: ( ( for N being non empty Subset of R holds card (min-classes N) = 1 ) implies ( R is connected & R \~ is well_founded ) )

assume that
A2: R is connected and
A3: R \~ is well_founded ; :: thesis: for N being non empty Subset of the carrier of R holds card (min-classes N) = 1
let N be non empty Subset of the carrier of R; :: thesis: card (min-classes N) = 1
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: for y being object holds
( ( y in min-classes N implies y in {x} ) & ( y in {x} implies y in min-classes N ) )

let y be object ; :: thesis: ( ( y in min-classes N implies y in {x} ) & ( y in {x} implies y in min-classes N ) )

hereby :: thesis: ( y in {x} implies y in min-classes N )

assume y in min-classes N ; :: thesis: y in {x}
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: ( [a,b] in the InternalRel of R & [b,a] in the InternalRel of R )

per cases ( a9 <= b9 or b9 <= a9 ) by A2, WAYBEL_0:def 29;

suppose A12: a9 <= b9 ; :: thesis: ( [a,b] in the InternalRel of R & [b,a] in the InternalRel of R )

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

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

per cases ( a = b or a <> b ) ;

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

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

end;

suppose A14: a <> b ; :: thesis: [b,a] in the InternalRel of R

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

assume not [b,a] in the InternalRel of R ; :: thesis: contradiction
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: verum

end;

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

end;

end;

end;

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

end;

suppose A15: b9 <= a9 ; :: thesis: ( [a,b] in the InternalRel of R & [b,a] in the InternalRel of R )

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

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

per cases ( a = b or a <> b ) ;

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

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

end;

suppose A17: a <> b ; :: thesis: [a,b] in the InternalRel of R

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

assume not [a,b] in the InternalRel of R ; :: thesis: contradiction
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: verum

end;

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

end;

end;

end;

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

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: verum

end;

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

end;

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

end;

assume A18: for N being non empty Subset of R holds card (min-classes N) = 1 ; :: thesis: ( R is connected & R \~ is well_founded )

now :: thesis: for a, b being Element of R st not a <= b holds
a >= b

let a, b be Element of R; :: thesis: ( not a <= b implies a >= b )
assume that
A19: not a <= b and
A20: not a >= b ; :: thesis: contradiction
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: for x being object holds
( ( x in min-classes {a,b} implies x in {{a},{b}} ) & ( x in {{a},{b}} implies x in min-classes {a,b} ) )

let x be object ; :: thesis: ( ( x in min-classes {a,b} implies x in {{a},{b}} ) & ( x in {{a},{b}} implies b₁ in min-classes {a,b} ) )
reconsider xx = x as set by TARSKI:1;

hereby :: thesis: ( x in {{a},{b}} implies b₁ in min-classes {a,b} )

assume x in min-classes {a,b} ; :: thesis: x in {{a},{b}}
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 ( y = a or y = b ) by A26, TARSKI:def 2;

suppose A27: y = a ; :: thesis: x in {{a},{b}}

now :: thesis: for z being object holds
( ( z in xx implies z in {a} ) & ( z in {a} implies z in xx ) )

let z be object ; :: thesis: ( ( z in xx implies z in {a} ) & ( z in {a} implies z in xx ) )

hereby :: thesis: ( z in {a} implies z in xx )

assume A28: z in xx ; :: thesis: z in {a}
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: z in {a}

per cases ( z = a or z = b ) by A30, TARSKI:def 2;

suppose z = a ; :: thesis: z in {a}

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

end;

suppose z = b ; :: thesis: z in {a}

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: verum

end;

end;

end;

hence z in {a} ; :: thesis: verum

end;

assume z in {a} ; :: thesis: z in xx
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: verum

end;

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

end;

suppose A33: y = b ; :: thesis: x in {{a},{b}}

now :: thesis: for z being object holds
( ( z in xx implies z in {b} ) & ( z in {b} implies z in xx ) )

let z be object ; :: thesis: ( ( z in xx implies z in {b} ) & ( z in {b} implies z in xx ) )

hereby :: thesis: ( z in {b} implies z in xx )

assume A34: z in xx ; :: thesis: z in {b}
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: z in {b}

per cases ( z = b or z = a ) by A36, TARSKI:def 2;

suppose z = b ; :: thesis: z in {b}

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

end;

suppose z = a ; :: thesis: z in {b}

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: verum

end;

end;

end;

hence z in {b} ; :: thesis: verum

end;

assume z in {b} ; :: thesis: z in xx
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: verum

end;

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

end;

end;

end;

assume A39: x in {{a},{b}} ; :: thesis: b₁ in min-classes {a,b}

per cases ( x = {a} or x = {b} ) by A39, TARSKI:def 2;

suppose A40: x = {a} ; :: thesis: b₁ in min-classes {a,b}

now :: thesis: ex a9 being Element of (R \~) st
( a9 is_minimal_wrt {a,b}, the InternalRel of (R \~) & x = (Class ((EqRel R),a9)) /\ {a,b} )

reconsider a9 = a as Element of (R \~) ;
take a9 = a9; :: thesis: ( a9 is_minimal_wrt {a,b}, the InternalRel of (R \~) & x = (Class ((EqRel R),a9)) /\ {a,b} )
A41: a9 in {a,b} by TARSKI:def 2;

now :: thesis: for y being set holds
( not y in {a,b} or not y <> a9 or not [y,a9] in the InternalRel of (R \~) )

assume ex y being set st
( y in {a,b} & y <> a9 & [y,a9] in the InternalRel of (R \~) ) ; :: thesis: contradiction
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: verum

end;

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

now :: thesis: for z being object holds
( ( z in xx implies z in (Class ((EqRel R),a)) /\ {a,b} ) & ( z in (Class ((EqRel R),a)) /\ {a,b} implies z in xx ) )

let z be object ; :: thesis: ( ( z in xx implies z in (Class ((EqRel R),a)) /\ {a,b} ) & ( z in (Class ((EqRel R),a)) /\ {a,b} implies b₁ in xx ) )

hereby :: thesis: ( z in (Class ((EqRel R),a)) /\ {a,b} implies b₁ in xx )

assume z in xx ; :: thesis: z in (Class ((EqRel R),a)) /\ {a,b}
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: verum

end;

assume A46: z in (Class ((EqRel R),a)) /\ {a,b} ; :: thesis: b₁ in xx
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 ( z = a or z = b ) by A48, TARSKI:def 2;

suppose z = a ; :: thesis: b₁ in xx

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

end;

suppose z = b ; :: thesis: b₁ in xx

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: verum

end;

end;

end;

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

end;

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

end;

suppose A49: x = {b} ; :: thesis: b₁ in min-classes {a,b}

now :: thesis: ex b9 being Element of (R \~) st
( b9 is_minimal_wrt {a,b}, the InternalRel of (R \~) & x = (Class ((EqRel R),b9)) /\ {a,b} )

reconsider b9 = b as Element of (R \~) ;
take b9 = b9; :: thesis: ( b9 is_minimal_wrt {a,b}, the InternalRel of (R \~) & x = (Class ((EqRel R),b9)) /\ {a,b} )
A50: b9 in {a,b} by TARSKI:def 2;

now :: thesis: for y being set holds
( not y in {a,b} or not y <> b9 or not [y,b9] in the InternalRel of (R \~) )

assume ex y being set st
( y in {a,b} & y <> b9 & [y,b9] in the InternalRel of (R \~) ) ; :: thesis: contradiction
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: verum

end;

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

now :: thesis: for z being object holds
( ( z in xx implies z in (Class ((EqRel R),b)) /\ {a,b} ) & ( z in (Class ((EqRel R),b)) /\ {a,b} implies z in xx ) )

let z be object ; :: thesis: ( ( z in xx implies z in (Class ((EqRel R),b)) /\ {a,b} ) & ( z in (Class ((EqRel R),b)) /\ {a,b} implies b₁ in xx ) )

hereby :: thesis: ( z in (Class ((EqRel R),b)) /\ {a,b} implies b₁ in xx )

assume z in xx ; :: thesis: z in (Class ((EqRel R),b)) /\ {a,b}
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: verum

end;

assume A55: z in (Class ((EqRel R),b)) /\ {a,b} ; :: thesis: b₁ in xx
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 ( z = b or z = a ) by A57, TARSKI:def 2;

suppose z = b ; :: thesis: b₁ in xx

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

end;

suppose z = a ; :: thesis: b₁ in xx

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: verum

end;

end;

end;

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

end;

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

end;

end;

end;

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

now :: thesis: not {a} = {b}

assume {a} = {b} ; :: thesis: contradiction
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: verum

end;

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

end;

hence R is connected by WAYBEL_0:def 29; :: thesis: R \~ is well_founded

now :: thesis: for N being Subset of R st N <> {} holds
ex x being object st x in min-classes N

let N be Subset of R; :: thesis: ( N <> {} implies ex x being object st x in min-classes N )
assume N <> {} ; :: thesis: ex x being object st x in min-classes N
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: verum

end;

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