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 set such that
A4: x in min-classes N by A3, Th21;
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

let y be set ; :: 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

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 by ORDERS_2:def 5;

now

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, ORDERS_2:def 5; :: thesis: verum

end;

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

now

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, ORDERS_2:def 5; :: 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 by ORDERS_2:def 5;

now

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, ORDERS_2:def 5; :: thesis: verum

end;

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

now

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, ORDERS_2:def 5; :: 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:1;
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

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, ORDERS_2:def 5;
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, ORDERS_2:def 5;
then A23: not [a,b] in the InternalRel of R ~ by RELAT_1:def 7;
set N9 = {a,b};
set MCN = {{a},{b}};

now

let x be set ; :: thesis: ( ( x in min-classes {a,b} implies x in {{a},{b}} ) & ( x in {{a},{b}} implies b₁ in min-classes {a,b} ) )

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

let z be set ; :: thesis: ( ( z in x implies z in {a} ) & ( z in {a} implies z in x ) )

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

assume A28: z in x ; :: 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

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 x
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 x by A25, A27, A32, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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

now

let z be set ; :: thesis: ( ( z in x implies z in {b} ) & ( z in {b} implies z in x ) )

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

assume A34: z in x ; :: 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

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 x
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 x by A25, A33, A38, XBOOLE_0:def 4; :: thesis: verum

end;

then x = {b} by TARSKI:1;
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

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

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, ORDERS_2:def 5; :: 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

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

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

assume z in x ; :: 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 x
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 x

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

end;

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

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 x by A22, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence x = (Class ((EqRel R),a9)) /\ {a,b} by TARSKI:1; :: 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

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

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, ORDERS_2:def 5; :: 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

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

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

assume z in x ; :: 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 x
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 x

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

end;

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

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 x by A23, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence x = (Class ((EqRel R),b9)) /\ {a,b} by TARSKI:1; :: 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:1;
then A58: card {{a},{b}} = 1 by A18;

now

assume {a} = {b} ; :: thesis: contradiction
then A59: a = b by ZFMISC_1:3;
R is reflexive by A1, Def3;
then the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 2;
hence contradiction by A21, A59, RELAT_2:def 1; :: 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

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

end;

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