let f be non constant standard special_circular_sequence; :: thesis: for i1, i2 being Element of NAT st 1 <= i1 & i1 <= i2 & i2 < len f holds
mid f,i2,i1 is_a_part<_of f,i2,i1
let i1, i2 be Element of NAT ; :: thesis: ( 1 <= i1 & i1 <= i2 & i2 < len f implies mid f,i2,i1 is_a_part<_of f,i2,i1 )
assume that
A1: 1 <= i1 and
A2: i1 <= i2 and
A3: i2 < len f ; :: thesis: mid f,i2,i1 is_a_part<_of f,i2,i1
Rev (mid f,i1,i2) is_a_part<_of f,i2,i1 by A1, A2, A3, Th41, Th43;
hence mid f,i2,i1 is_a_part<_of f,i2,i1 by Th30; :: thesis: verum