set p = ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>;
A1: ( len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) = 4 & (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 1 = 1 & (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 2 = 2 & (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 3 = 3 & (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 4 = 1 ) by FINSEQ_1:87;
reconsider VERTICES = the carrier of TriangleGraph as non empty set by Th46;
reconsider One = 1, Two = 2, Three = 3 as Element of VERTICES by Th46, ENUMSET1:def 1, FINSEQ_3:1;
reconsider o = 1 as Element of the carrier of TriangleGraph by Th46, ENUMSET1:def 1, FINSEQ_3:1;
reconsider ONE = <*One*>, TWO = <*Two*>, THREE = <*Three*> as FinSequence of the carrier of TriangleGraph ;
( ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> = ((ONE ^ TWO) ^ THREE) ^ ONE & (ONE ^ TWO) ^ THREE is FinSequence of the carrier of TriangleGraph ) ;
then reconsider pp = ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> as Element of the carrier of TriangleGraph * by FINSEQ_1:def 11;

A2: now

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) implies {(pp . b₁),(pp . (b₁ + 1))} in the SEdges of TriangleGraph )
assume ( 1 <= i & i < len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) ) ; :: thesis: {(pp . b₁),(pp . (b₁ + 1))} in the SEdges of TriangleGraph
then ( 1 <= i & i < 3 + 1 ) by FINSEQ_1:87;
then ( 1 <= i & i <= 3 ) by NAT_1:13;
then A3: i in Seg 3 by FINSEQ_1:3;

per cases ( i = 1 or i = 2 or i = 3 ) by A3, ENUMSET1:def 1, FINSEQ_3:1;

suppose i = 1 ; :: thesis: {(pp . b₁),(pp . (b₁ + 1))} in the SEdges of TriangleGraph

hence {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A1, Th46, ENUMSET1:def 1; :: thesis: verum

end;

suppose i = 2 ; :: thesis: {(pp . b₁),(pp . (b₁ + 1))} in the SEdges of TriangleGraph

hence {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A1, Th46, ENUMSET1:def 1; :: thesis: verum

end;

suppose i = 3 ; :: thesis: {(pp . b₁),(pp . (b₁ + 1))} in the SEdges of TriangleGraph

hence {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A1, Th46, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

now

let i, j be Element of NAT ; :: thesis: ( 1 <= i & i < len pp & i < j & j < len pp implies ( pp . b₁ <> pp . b₂ & {(pp . b₁),(pp . (b₁ + 1))} <> {(pp . b₂),(pp . (b₂ + 1))} ) )
assume ( 1 <= i & i < len pp & i < j & j < len pp ) ; :: thesis: ( pp . b₁ <> pp . b₂ & {(pp . b₁),(pp . (b₁ + 1))} <> {(pp . b₂),(pp . (b₂ + 1))} )
then A4: ( 1 <= i & i < 3 + 1 & i < j & j < 3 + 1 ) by FINSEQ_1:87;
then A5: ( 1 <= i & i <= 3 & i < j & j <= 3 ) by NAT_1:13;
A6: ( 1 <= i + 1 & i + 1 <= j & j <= 3 ) by A4, NAT_1:13;
then A7: ( i in Seg 3 & j in nat_interval (i + 1),3 ) by A5, FINSEQ_1:3;

per cases ( i = 1 or i = 2 or i = 3 ) by A7, ENUMSET1:def 1, FINSEQ_3:1;

suppose A8: i = 1 ; :: thesis: ( pp . b₁ <> pp . b₂ & {(pp . b₁),(pp . (b₁ + 1))} <> {(pp . b₂),(pp . (b₂ + 1))} )

then A9: pp . i = o by FINSEQ_1:87;
( j = 2 or ( 2 < j & j <= 3 ) ) by A6, A8, XXREAL_0:1;
then A10: ( j = 2 or ( 2 + 1 <= j & j <= 3 ) ) by NAT_1:13;

now

per cases ( j = 2 or j = 3 ) by A10, XXREAL_0:1;

suppose A11: j = 2 ; :: thesis: ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} )

hence pp . i <> pp . j by A9, FINSEQ_1:87; :: thesis: {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))}
thus {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} by A1, A8, A11, ZFMISC_1:10; :: thesis: verum

end;

suppose A12: j = 3 ; :: thesis: ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} )

hence pp . i <> pp . j by A9, FINSEQ_1:87; :: thesis: {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))}
thus {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} by A1, A8, A12, ZFMISC_1:10; :: thesis: verum

end;

end;

end;

hence ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) ; :: thesis: verum

end;

suppose A13: i = 2 ; :: thesis: ( pp . b₁ <> pp . b₂ & {(pp . b₁),(pp . (b₁ + 1))} <> {(pp . b₂),(pp . (b₂ + 1))} )

then j = 3 by A6, XXREAL_0:1;
hence ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) by A1, A13, ZFMISC_1:10; :: thesis: verum

end;

suppose i = 3 ; :: thesis: ( pp . b₁ <> pp . b₂ & {(pp . b₁),(pp . (b₁ + 1))} <> {(pp . b₂),(pp . (b₂ + 1))} )

hence ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) by A4, NAT_1:13; :: thesis: verum

end;

end;

end;

then pp is_path_of o,o by A1, A2, Def12;
then pp in PATHS o,o ;
hence ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> is_cycle_of TriangleGraph by Def14; :: thesis: verum