let A be RelStr ; :: thesis: for B being Subset of A

for s being FinSequence of A st s is B -desc_ordering holds

the InternalRel of A is_connected_in B

let B be Subset of A; :: thesis: for s being FinSequence of A st s is B -desc_ordering holds

the InternalRel of A is_connected_in B

let s be FinSequence of A; :: thesis: ( s is B -desc_ordering implies the InternalRel of A is_connected_in B )

assume s is B -desc_ordering ; :: thesis: the InternalRel of A is_connected_in B

then Rev (Rev s) is B -desc_ordering ;

then Rev s is B -asc_ordering by Th75;

hence the InternalRel of A is_connected_in B by Th83; :: thesis: verum

for s being FinSequence of A st s is B -desc_ordering holds

the InternalRel of A is_connected_in B

let B be Subset of A; :: thesis: for s being FinSequence of A st s is B -desc_ordering holds

the InternalRel of A is_connected_in B

let s be FinSequence of A; :: thesis: ( s is B -desc_ordering implies the InternalRel of A is_connected_in B )

assume s is B -desc_ordering ; :: thesis: the InternalRel of A is_connected_in B

then Rev (Rev s) is B -desc_ordering ;

then Rev s is B -asc_ordering by Th75;

hence the InternalRel of A is_connected_in B by Th83; :: thesis: verum