let f be non constant standard special_circular_sequence; :: thesis: for i1, i2 being Element of NAT st 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & i1 <> i2 holds
ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )
let i1, i2 be Element of NAT ; :: thesis: ( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & i1 <> i2 implies ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) ) )
assume that
A1: 1 <= i1 and
A2: i1 + 1 <= len f and
A3: 1 <= i2 and
A4: i2 + 1 <= len f and
A5: i1 <> i2 ; :: thesis: ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )

now

per cases ( i1 <= i2 or i1 > i2 ) ;

case A6: i1 <= i2 ; :: thesis: ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )

set h1 = mid f,i1,i2;
set h2 = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2);
A7: i2 < len f by A4, NAT_1:13;
then A8: mid f,i1,i2 is_a_part>_of f,i1,i2 by A1, A6, Th43;
then A9: mid f,i1,i2 is_a_part_of f,i1,i2 by Def4;
A10: i1 < i2 by A5, A6, XXREAL_0:1;
then A11: L~ (mid f,i1,i2) is_S-P_arc_joining f /. i1,f /. i2 by A8, Th56;
A12: for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = mid f,i1,i2 or g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )

proof

let g be FinSequence of (TOP-REAL 2); :: thesis: ( not g is_a_part_of f,i1,i2 or g = mid f,i1,i2 or g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )
assume A13: g is_a_part_of f,i1,i2 ; :: thesis: ( g = mid f,i1,i2 or g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )

now

per cases ( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 ) by A13, Def4;

case g is_a_part>_of f,i1,i2 ; :: thesis: ( g = mid f,i1,i2 or g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )

hence ( g = mid f,i1,i2 or g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) ) by A6, Th37; :: thesis: verum

end;

case g is_a_part<_of f,i1,i2 ; :: thesis: ( g = mid f,i1,i2 or g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )

hence ( g = mid f,i1,i2 or g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) ) by A10, Th40; :: thesis: verum

end;

end;

end;

hence ( g = mid f,i1,i2 or g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) ) ; :: thesis: verum

end;

A14: (L~ (mid f,i1,i2)) \/ (L~ ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2))) = L~ f by A1, A10, A7, Th55;
A15: (L~ (mid f,i1,i2)) /\ (L~ ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2))) = {(f . i1),(f . i2)} by A1, A10, A7, Th55;
(mid f,i1,1) ^ (mid f,((len f) -' 1),i2) is_a_part<_of f,i1,i2 by A1, A10, A7, Th46;
then A16: (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) is_a_part_of f,i1,i2 by Def4;
then L~ ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) is_S-P_arc_joining f /. i1,f /. i2 by A5, Th60;
hence ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) ) by A9, A16, A15, A14, A11, A12; :: thesis: verum

end;

case A17: i1 > i2 ; :: thesis: ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )

set h1 = mid f,i2,i1;
set h2 = (mid f,i2,1) ^ (mid f,((len f) -' 1),i1);
set h3 = Rev (mid f,i2,i1);
set h4 = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1));
A18: L~ (mid f,i2,i1) = L~ (Rev (mid f,i2,i1)) by SPPOL_2:22;
A19: for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = Rev (mid f,i2,i1) or g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) )

proof

let g be FinSequence of (TOP-REAL 2); :: thesis: ( not g is_a_part_of f,i1,i2 or g = Rev (mid f,i2,i1) or g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) )
assume A20: g is_a_part_of f,i1,i2 ; :: thesis: ( g = Rev (mid f,i2,i1) or g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) )

now

per cases ( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 ) by A20, Def4;

case g is_a_part>_of f,i1,i2 ; :: thesis: ( g = Rev (mid f,i2,i1) or g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) )

then Rev g is_a_part<_of f,i2,i1 by Th41;
then Rev g = (mid f,i2,1) ^ (mid f,((len f) -' 1),i1) by A17, Th40;
hence ( g = Rev (mid f,i2,i1) or g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) ) by FINSEQ_6:29; :: thesis: verum

end;

case g is_a_part<_of f,i1,i2 ; :: thesis: ( g = Rev (mid f,i2,i1) or g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) )

then Rev g is_a_part>_of f,i2,i1 by Th42;
then Rev g = mid f,i2,i1 by A17, Th37;
hence ( g = Rev (mid f,i2,i1) or g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) ) by FINSEQ_6:29; :: thesis: verum

end;

end;

end;

hence ( g = Rev (mid f,i2,i1) or g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) ) ; :: thesis: verum

end;

A21: i1 < len f by A2, NAT_1:13;
then mid f,i2,i1 is_a_part>_of f,i2,i1 by A3, A17, Th43;
then A22: L~ (Rev (mid f,i2,i1)) is_S-P_arc_joining f /. i1,f /. i2 by A17, Th41, Th59;
(L~ (mid f,i2,i1)) \/ (L~ ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1))) = L~ f by A3, A17, A21, Th55;
then A23: (L~ (Rev (mid f,i2,i1))) \/ (L~ (Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)))) = L~ f by A18, SPPOL_2:22;
(L~ (mid f,i2,i1)) /\ (L~ ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1))) = {(f . i2),(f . i1)} by A3, A17, A21, Th55;
then A24: (L~ (Rev (mid f,i2,i1))) /\ (L~ (Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)))) = {(f . i1),(f . i2)} by A18, SPPOL_2:22;
Rev (mid f,i2,i1) is_a_part<_of f,i1,i2 by A3, A17, A21, Th41, Th43;
then A25: Rev (mid f,i2,i1) is_a_part_of f,i1,i2 by Def4;
Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) is_a_part>_of f,i1,i2 by A3, A17, A21, Th42, Th46;
then A26: Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) is_a_part_of f,i1,i2 by Def4;
then L~ (Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1))) is_S-P_arc_joining f /. i1,f /. i2 by A5, Th60;
hence ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) ) by A25, A26, A24, A23, A22, A19; :: thesis: verum

end;

end;

end;

hence ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) ) ; :: thesis: verum