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 S1[ 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: S1[ 0 ]
proof
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;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[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
proof
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
per cases ( k = 0 or k > 0 ) ;
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 ;
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 ;
take s ; :: thesis: s is C -asc_ordering
thus s is C -asc_ordering by ; :: thesis: verum
end;
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 ;
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) - () by
.= (k + 1) - 1 by
.= k ;
then consider s1 being FinSequence of A such that
A14: s1 is D -asc_ordering by ;
A15: not x in D by ZFMISC_1:56;
A16: for y being Element of A st y in D holds
x <= y
proof
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 ;
y in C by ;
hence x <= y by ; :: thesis: verum
end;
C = D \/ {x} by ;
then consider s2 being FinSequence of A such that
A19: ( s2 = <*x*> ^ s1 & s2 is C -asc_ordering ) by ;
take s2 ; :: thesis: s2 is C -asc_ordering
thus s2 is C -asc_ordering by A19; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A20: for k being Nat holds S1[k] from NAT_1:sch 2(A2, A4);
reconsider cardB = card B as Nat ;
S1[cardB] by A20;
hence ex s being FinSequence of A st s is B -asc_ordering ; :: thesis: verum