let A be transitive RelStr ; :: thesis:
let B be finite Subset of A; :: thesis:
assume A1: the InternalRel of A is_connected_in B ; :: thesis:
defpred S₁[ 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₁[ 0 ]

let C be Subset of A; :: thesis:
assume ( C c= B & card C = 0 ) ; :: thesis:
then A3: C = {} the carrier of A ;
reconsider s = <*> the carrier of A as FinSequence of A ;
take s ; :: thesis:
thus s is C -asc_ordering by A3; :: thesis:

end;

A4: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A5: S₁[k] ; :: thesis:
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

let C be Subset of A; :: thesis:
assume A6: ( C c= B & card C = k + 1 ) ; :: thesis:

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:
thus s is C -asc_ordering by A9, Th82; :: thesis:

end;

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

end;

end;

hence S₁[k + 1] ; :: thesis:

end;