let A be transitive RelStr ; :: thesis: for B being finite Subset of A st the InternalRel of A is_connected_in B holds

ex s being FinSequence of A st s is B -asc_ordering

let B be finite Subset of A; :: thesis: ( the InternalRel of A is_connected_in B implies ex s being FinSequence of A st s is B -asc_ordering )

assume A1: the InternalRel of A is_connected_in B ; :: thesis: ex s being FinSequence of A st s is B -asc_ordering

defpred S_{1}[ Nat] means for C being Subset of A st C c= B & card C = $1 holds

ex s being FinSequence of A st s is C -asc_ordering ;

A2: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A2, A4);

reconsider cardB = card B as Nat ;

S_{1}[cardB]
by A20;

hence ex s being FinSequence of A st s is B -asc_ordering ; :: thesis: verum

ex s being FinSequence of A st s is B -asc_ordering

let B be finite Subset of A; :: thesis: ( the InternalRel of A is_connected_in B implies ex s being FinSequence of A st s is B -asc_ordering )

assume A1: the InternalRel of A is_connected_in B ; :: thesis: ex s being FinSequence of A st s is B -asc_ordering

defpred S

ex s being FinSequence of A st s is C -asc_ordering ;

A2: S

proof

A4:
for k being Nat st S
let C be Subset of A; :: thesis: ( C c= B & card C = 0 implies ex s being FinSequence of A st s is C -asc_ordering )

assume ( C c= B & card C = 0 ) ; :: thesis: ex s being FinSequence of A st s is C -asc_ordering

then A3: C = {} the carrier of A ;

reconsider s = <*> the carrier of A as FinSequence of A ;

take s ; :: thesis: s is C -asc_ordering

thus s is C -asc_ordering by A3; :: thesis: verum

end;assume ( C c= B & card C = 0 ) ; :: thesis: ex s being FinSequence of A st s is C -asc_ordering

then A3: C = {} the carrier of A ;

reconsider s = <*> the carrier of A as FinSequence of A ;

take s ; :: thesis: s is C -asc_ordering

thus s is C -asc_ordering by A3; :: thesis: verum

S

proof

A20:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S_{1}[k]
; :: thesis: S_{1}[k + 1]

for C being Subset of A st C c= B & card C = k + 1 holds

ex s being FinSequence of A st s is C -asc_ordering_{1}[k + 1]
; :: thesis: verum

end;assume A5: S

for C being Subset of A st C c= B & card C = k + 1 holds

ex s being FinSequence of A st s is C -asc_ordering

proof

hence
S
let C be Subset of A; :: thesis: ( C c= B & card C = k + 1 implies ex s being FinSequence of A st s is C -asc_ordering )

assume A6: ( C c= B & card C = k + 1 ) ; :: thesis: ex s being FinSequence of A st s is C -asc_ordering

end;assume A6: ( C c= B & card C = k + 1 ) ; :: thesis: ex s being FinSequence of A st s is C -asc_ordering

per cases
( k = 0 or k > 0 )
;

end;

suppose
k = 0
; :: thesis: ex s being FinSequence of A st s is C -asc_ordering

then A7:
card C = 1
by A6;

set x = the Element of C;

A8: not C is empty by A7;

then A9: { the Element of C} = C by A7, Th2;

then the Element of C in C ;

then reconsider x = the Element of C as Element of A ;

set s = <*x*>;

reconsider s = <*x*> as FinSequence of A by A8, FINSEQ_1:74;

take s ; :: thesis: s is C -asc_ordering

thus s is C -asc_ordering by A9, Th82; :: thesis: verum

end;set x = the Element of C;

A8: not C is empty by A7;

then A9: { the Element of C} = C by A7, Th2;

then the Element of C in C ;

then reconsider x = the Element of C as Element of A ;

set s = <*x*>;

reconsider s = <*x*> as FinSequence of A by A8, FINSEQ_1:74;

take s ; :: thesis: s is C -asc_ordering

thus s is C -asc_ordering by A9, Th82; :: thesis: verum

suppose
k > 0
; :: thesis: ex s being FinSequence of A st s is C -asc_ordering

A10:
not C is empty
by A6;

reconsider C = C as finite Subset of A by A6;

the InternalRel of A is_connected_in C by A1, A6, Th16;

then consider x being Element of A such that

A11: ( x in C & ( for y being Element of A st y in C & x <> y holds

x <= y ) ) by A10, Th31;

set D = C \ {x};

reconsider D = C \ {x} as Subset of A ;

A12: D c= C by XBOOLE_1:36;

then A13: D c= B by A6;

card D = (card C) - (card {x}) by A11, ZFMISC_1:31, CARD_2:44

.= (k + 1) - 1 by A6, CARD_1:30

.= k ;

then consider s1 being FinSequence of A such that

A14: s1 is D -asc_ordering by A5, A13;

A15: not x in D by ZFMISC_1:56;

A16: for y being Element of A st y in D holds

x <= y

then consider s2 being FinSequence of A such that

A19: ( s2 = <*x*> ^ s1 & s2 is C -asc_ordering ) by A14, A16, A15, Th85;

take s2 ; :: thesis: s2 is C -asc_ordering

thus s2 is C -asc_ordering by A19; :: thesis: verum

end;reconsider C = C as finite Subset of A by A6;

the InternalRel of A is_connected_in C by A1, A6, Th16;

then consider x being Element of A such that

A11: ( x in C & ( for y being Element of A st y in C & x <> y holds

x <= y ) ) by A10, Th31;

set D = C \ {x};

reconsider D = C \ {x} as Subset of A ;

A12: D c= C by XBOOLE_1:36;

then A13: D c= B by A6;

card D = (card C) - (card {x}) by A11, ZFMISC_1:31, CARD_2:44

.= (k + 1) - 1 by A6, CARD_1:30

.= k ;

then consider s1 being FinSequence of A such that

A14: s1 is D -asc_ordering by A5, A13;

A15: not x in D by ZFMISC_1:56;

A16: for y being Element of A st y in D holds

x <= y

proof

C = D \/ {x}
by A11, ZFMISC_1:116;
let y be Element of A; :: thesis: ( y in D implies x <= y )

assume A17: y in D ; :: thesis: x <= y

A18: x <> y by A17, ZFMISC_1:56;

y in C by A17, A12;

hence x <= y by A11, A18; :: thesis: verum

end;assume A17: y in D ; :: thesis: x <= y

A18: x <> y by A17, ZFMISC_1:56;

y in C by A17, A12;

hence x <= y by A11, A18; :: thesis: verum

then consider s2 being FinSequence of A such that

A19: ( s2 = <*x*> ^ s1 & s2 is C -asc_ordering ) by A14, A16, A15, Th85;

take s2 ; :: thesis: s2 is C -asc_ordering

thus s2 is C -asc_ordering by A19; :: thesis: verum

reconsider cardB = card B as Nat ;

S

hence ex s being FinSequence of A st s is B -asc_ordering ; :: thesis: verum