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 IR' = 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 A2: ( R is connected & 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
A3: x in min-classes N by A2, Th21;
consider a being Element of (R \~ ) such that
A4: a is_minimal_wrt N,the InternalRel of (R \~ ) and
A5: x = (Class (EqRel R),a) /\ N by A3, Def8;
A6: ( a in N & ( for b being Element of (R \~ ) holds
( not b in N or not b <> a or not [b,a] in the InternalRel of (R \~ ) ) ) ) by A4, WAYBEL_4:def 26;

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
A7: b is_minimal_wrt N,the InternalRel of (R \~ ) and
A8: y = (Class (EqRel R),b) /\ N by Def8;
A9: ( b in N & ( for a being Element of (R \~ ) holds
( not a in N or not a <> b or not [a,b] in the InternalRel of (R \~ ) ) ) ) by A7, WAYBEL_4:def 26;
reconsider a' = a as Element of R ;
reconsider b' = b as Element of R ;

A10: now

per cases ( a' <= b' or b' <= a' ) by A2, WAYBEL_0:def 29;

suppose A11: a' <= b' ; :: thesis: ( [a,b] in the InternalRel of R & [b,a] in the InternalRel of R )

then A12: [a,b] in the InternalRel of R by ORDERS_2:def 9;

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

end;

suppose A13: 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 A12, XBOOLE_0:def 5;
hence contradiction by A6, A7, A13, WAYBEL_4:def 26; :: 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 A11, ORDERS_2:def 9; :: thesis: verum

end;

suppose A14: b' <= a' ; :: thesis: ( [a,b] in the InternalRel of R & [b,a] in the InternalRel of R )

then A15: [b,a] in the InternalRel of R by ORDERS_2:def 9;

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

end;

suppose A16: 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 A15, XBOOLE_0:def 5;
hence contradiction by A4, A9, A16, WAYBEL_4:def 26; :: 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 A14, ORDERS_2:def 9; :: 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 A10, XBOOLE_0:def 4;
then [b,a] in EqRel R by A1, Def4;
then b in Class (EqRel R),a by EQREL_1:27;
then Class (EqRel R),b = Class (EqRel R),a by EQREL_1:31;
hence y in {x} by A5, A8, TARSKI:def 1; :: thesis: verum

end;

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

end;

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

end;

assume A17: 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 A18: ( not a <= b & not a >= b ) ; :: thesis: contradiction
then A19: not [a,b] in the InternalRel of R by ORDERS_2:def 9;
then A20: not [b,a] in the InternalRel of R ~ by RELAT_1:def 7;
not [b,a] in the InternalRel of R by A18, ORDERS_2:def 9;
then A21: not [a,b] in the InternalRel of R ~ by RELAT_1:def 7;
set N' = {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
A22: y is_minimal_wrt {a,b},the InternalRel of (R \~ ) and
A23: x = (Class (EqRel R),y) /\ {a,b} by Def8;
A24: ( y in {a,b} & ( for z being Element of (R \~ ) holds
( not z in {a,b} or not z <> y or not [z,y] in the InternalRel of (R \~ ) ) ) ) by A22, WAYBEL_4:def 26;

per cases ( y = a or y = b ) by A24, TARSKI:def 2;

suppose A25: 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 z in x ; :: thesis: z in {a}
then A26: ( z in Class (EqRel R),a & z in {a,b} ) by A23, A25, XBOOLE_0:def 4;

now

per cases ( z = a or z = b ) by A26, 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 A26, EQREL_1:27;
then [b,a] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, Def4;
hence z in {a} by A20, 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 A27: z = a by TARSKI:def 1;
then A28: z in {a,b} by TARSKI:def 2;
z in Class (EqRel R),a by A27, EQREL_1:28;
hence z in x by A23, A25, A28, 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 A29: 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 z in x ; :: thesis: z in {b}
then A30: ( z in Class (EqRel R),b & z in {a,b} ) by A23, A29, XBOOLE_0:def 4;

now

per cases ( z = b or z = a ) by A30, 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 A30, EQREL_1:27;
then [a,b] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, Def4;
hence z in {b} by A19, 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 A31: z = b by TARSKI:def 1;
then A32: z in {a,b} by TARSKI:def 2;
z in Class (EqRel R),b by A31, EQREL_1:28;
hence z in x by A23, A29, A32, 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 A33: x in {{a},{b}} ; :: thesis: b₁ in min-classes {a,b}

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

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

now

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

now

assume ex y being set st
( y in {a,b} & y <> a' & [y,a'] in the InternalRel of (R \~ ) ) ; :: thesis: contradiction
then consider y being set such that
A36: y in {a,b} and
A37: ( y <> a' & [y,a'] in the InternalRel of (R \~ ) ) ;
y = b by A36, A37, TARSKI:def 2;
hence contradiction by A18, A37, ORDERS_2:def 9; :: thesis: verum

end;

hence a' is_minimal_wrt {a,b},the InternalRel of (R \~ ) by A35, WAYBEL_4:def 26; :: thesis: x = (Class (EqRel R),a') /\ {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 A38: z = a by A34, TARSKI:def 1;
then z in Class (EqRel R),a by EQREL_1:28;
hence z in (Class (EqRel R),a) /\ {a,b} by A35, A38, XBOOLE_0:def 4; :: thesis: verum

end;

assume z in (Class (EqRel R),a) /\ {a,b} ; :: thesis: b₁ in x
then A39: ( z in Class (EqRel R),a & z in {a,b} ) by XBOOLE_0:def 4;

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

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

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

end;

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

then [b,a] in EqRel R by A39, EQREL_1:27;
then [b,a] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, Def4;
hence z in x by A20, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

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

end;

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

end;

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

now

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

now

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

end;

hence b' is_minimal_wrt {a,b},the InternalRel of (R \~ ) by A41, WAYBEL_4:def 26; :: thesis: x = (Class (EqRel R),b') /\ {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 A44: z = b by A40, TARSKI:def 1;
then z in Class (EqRel R),b by EQREL_1:28;
hence z in (Class (EqRel R),b) /\ {a,b} by A41, A44, XBOOLE_0:def 4; :: thesis: verum

end;

assume z in (Class (EqRel R),b) /\ {a,b} ; :: thesis: b₁ in x
then A45: ( z in Class (EqRel R),b & z in {a,b} ) by XBOOLE_0:def 4;

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

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

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

end;

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

then [a,b] in EqRel R by A45, EQREL_1:27;
then [a,b] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, Def4;
hence z in x by A21, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

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

now

assume {a} = {b} ; :: thesis: contradiction
then A47: a = b by ZFMISC_1:6;
R is reflexive by A1, Def3;
then the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 4;
hence contradiction by A19, A47, RELAT_2:def 1; :: thesis: verum

end;

hence contradiction by A46, CARD_2:76; :: 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 A48: N <> {} ; :: thesis: ex x being set st x in min-classes N
card (min-classes N) = 1 by A17, A48;
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