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