let A be RelStr ; :: thesis: for B being Subset of A
for s being FinSequence of A st s is B -asc_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 -asc_ordering holds
the InternalRel of A is_connected_in B
let s be FinSequence of A; :: thesis: ( s is B -asc_ordering implies the InternalRel of A is_connected_in B )
assume A1: s is B -asc_ordering ; :: thesis: the InternalRel of A is_connected_in B
then A2: s is weakly-ascending ;
for x, y being object st x in B & y in B & x <> y & not [x,y] in the InternalRel of A holds
[y,x] in the InternalRel of A
proof
let x, y be object ; :: thesis: ( x in B & y in B & x <> y & not [x,y] in the InternalRel of A implies [y,x] in the InternalRel of A )
assume that
A3: ( x in B & y in B ) and
A4: x <> y ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
reconsider x = x, y = y as Element of A by A3;
A5: ( x in rng s & y in rng s ) by A1, A3;
consider i being Nat such that
A6: i in dom s and
A7: x = s . i by FINSEQ_2:10, A5;
A8: x = s /. i by A6, A7, PARTFUN1:def 6;
consider j being Nat such that
A9: j in dom s and
A10: y = s . j by FINSEQ_2:10, A5;
A11: y = s /. j by A9, A10, PARTFUN1:def 6;
per cases ( i < j or i = j or j < i ) by XXREAL_0:1;
suppose i < j ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A6, A9, A8, A11, A2, ORDERS_2:def 5; :: thesis: verum
end;
suppose i = j ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A7, A10, A4; :: thesis: verum
end;
suppose j < i ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A6, A9, A8, A11, A2, ORDERS_2:def 5; :: thesis: verum
end;
end;
end;
hence the InternalRel of A is_connected_in B by RELAT_2:def 6; :: thesis: verum