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

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

hence
the InternalRel of A is_connected_in B
by RELAT_2:def 6; :: thesis: verum
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;

end;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;

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 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;