reconsider o = 1 as Element of the carrier of TriangleGraph by Th34, ENUMSET1:def 1, FINSEQ_3:1;
reconsider VERTICES = the carrier of TriangleGraph as non empty set by Th34;
set p = ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>;
A1: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 1 = 1 by FINSEQ_1:66;
reconsider One = 1, Two = 2, Three = 3 as Element of VERTICES by Th34, ENUMSET1:def 1, FINSEQ_3:1;
A2: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 2 = 2 by FINSEQ_1:66;
reconsider ONE = <*One*>, TWO = <*Two*>, THREE = <*Three*> as FinSequence of the carrier of TriangleGraph ;
((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> = ((ONE ^ TWO) ^ THREE) ^ ONE ;
then reconsider pp = ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> as Element of the carrier of TriangleGraph * by FINSEQ_1:def 11;
A3: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 3 = 3 by FINSEQ_1:66;
A4: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 4 = 1 by FINSEQ_1:66;
A5: now :: thesis: for i being Element of NAT st 1 <= i & i < len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) holds
{(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) implies {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph )
assume that
A6: 1 <= i and
A7: i < len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) ; :: thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
i < 3 + 1 by A7, FINSEQ_1:66;
then i <= 3 by NAT_1:13;
then A8: i in Seg 3 by A6;
per cases ( i = 1 or i = 2 or i = 3 ) by A8, ENUMSET1:def 1, FINSEQ_3:1;
suppose i = 1 ; :: thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
hence {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A1, A2, Th34, ENUMSET1:def 1; :: thesis: verum
end;
suppose i = 2 ; :: thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
hence {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A2, A3, Th34, ENUMSET1:def 1; :: thesis: verum
end;
suppose i = 3 ; :: thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
hence {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A3, A4, Th34, ENUMSET1:def 1; :: thesis: verum
end;
end;
end;
A9: now :: thesis: for i, j being Element of NAT st 1 <= i & i < len pp & i < j & j < len pp holds
( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} )
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i < len pp & i < j & j < len pp implies ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} ) )
assume that
A10: 1 <= i and
A11: i < len pp and
A12: i < j and
A13: j < len pp ; :: thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
A14: i + 1 <= j by A12, NAT_1:13;
i < 3 + 1 by A11, FINSEQ_1:66;
then i <= 3 by NAT_1:13;
then A15: i in Seg 3 by A10;
A16: j < 3 + 1 by A13, FINSEQ_1:66;
then A17: j <= 3 by NAT_1:13;
per cases ( i = 1 or i = 2 or i = 3 ) by A15, ENUMSET1:def 1, FINSEQ_3:1;
suppose A18: i = 1 ; :: thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
then A19: pp . i = o by FINSEQ_1:66;
( j = 2 or ( 2 < j & j <= 3 ) ) by A16, A14, A18, NAT_1:13, XXREAL_0:1;
then A20: ( j = 2 or ( 2 + 1 <= j & j <= 3 ) ) by NAT_1:13;
now :: thesis: ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} )
per cases ( j = 2 or j = 3 ) by A20, XXREAL_0:1;
suppose A21: j = 2 ; :: thesis: ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} )
hence pp . i <> pp . j by A19, FINSEQ_1:66; :: thesis: {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))}
thus {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} by A1, A2, A3, A18, A21, ZFMISC_1:6; :: thesis: verum
end;
suppose A22: j = 3 ; :: thesis: ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} )
hence pp . i <> pp . j by A19, FINSEQ_1:66; :: thesis: {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))}
thus {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} by A1, A2, A3, A18, A22, ZFMISC_1:6; :: thesis: verum
end;
end;
end;
hence ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) ; :: thesis: verum
end;
suppose A23: i = 2 ; :: thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
then j = 3 by A14, A17, XXREAL_0:1;
hence ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) by A2, A3, A4, A23, ZFMISC_1:6; :: thesis: verum
end;
suppose i = 3 ; :: thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
hence ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) by A12, A16, NAT_1:13; :: thesis: verum
end;
end;
end;
pp is_path_of o,o by A4, A5, A9, FINSEQ_1:66;
then pp in PATHS (o,o) ;
hence ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> is_cycle_of TriangleGraph ; :: thesis: verum