consider ee being finite Subset of (TWOELEMENTSETS (Seg 3)) such that
A1: ee = { {i,j} where i, j is Element of NAT : ( i in Seg 3 & j in Seg 3 & i <> j ) } and
A2: TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) by Def13;
take ee ; :: thesis: ( ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) )

now :: thesis: for a being object st a in ee holds
a in {.{.1,2.},{.2,3.},{.3,1.}.}

let a be object ; :: thesis: ( a in ee implies b₁ in {.{.1,2.},{.2,3.},{.3,1.}.} )
assume a in ee ; :: thesis: b₁ in {.{.1,2.},{.2,3.},{.3,1.}.}
then consider i, j being Element of NAT such that
A3: a = {i,j} and
A4: i in Seg 3 and
A5: j in Seg 3 and
A6: i <> j by A1;

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

suppose A7: i = 1 ; :: thesis: b₁ in {.{.1,2.},{.2,3.},{.3,1.}.}

now :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

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

suppose j = 1 ; :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6, A7; :: thesis: verum

end;

suppose j = 2 ; :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A7, ENUMSET1:def 1; :: thesis: verum

end;

suppose j = 3 ; :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A7, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} ; :: thesis: verum

end;

suppose A8: i = 2 ; :: thesis: b₁ in {.{.1,2.},{.2,3.},{.3,1.}.}

now :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

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

suppose j = 1 ; :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A8, ENUMSET1:def 1; :: thesis: verum

end;

suppose j = 2 ; :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6, A8; :: thesis: verum

end;

suppose j = 3 ; :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A8, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} ; :: thesis: verum

end;

suppose A9: i = 3 ; :: thesis: b₁ in {.{.1,2.},{.2,3.},{.3,1.}.}

now :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

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

suppose j = 1 ; :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A9, ENUMSET1:def 1; :: thesis: verum

end;

suppose j = 2 ; :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A9, ENUMSET1:def 1; :: thesis: verum

end;

suppose j = 3 ; :: thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6, A9; :: thesis: verum

end;

end;

end;

hence a in {.{.1,2.},{.2,3.},{.3,1.}.} ; :: thesis: verum

end;

end;

end;

then A10: ee c= {.{.1,2.},{.2,3.},{.3,1.}.} ;

now :: thesis: for e being object st e in {.{.1,2.},{.2,3.},{.3,1.}.} holds
e in ee

let e be object ; :: thesis: ( e in {.{.1,2.},{.2,3.},{.3,1.}.} implies b₁ in ee )
assume A11: e in {.{.1,2.},{.2,3.},{.3,1.}.} ; :: thesis: b₁ in ee

per cases ( e = {1,2} or e = {2,3} or e = {3,1} ) by A11, ENUMSET1:def 1;

suppose A12: e = {1,2} ; :: thesis: b₁ in ee

now :: thesis: ex i, j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )

take i = 1; :: thesis: ex j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
take j = 2; :: thesis: ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
thus e = {i,j} by A12; :: thesis: ( i in Seg 3 & j in Seg 3 & i <> j )
thus ( i in Seg 3 & j in Seg 3 ) ; :: thesis: i <> j
thus i <> j ; :: thesis: verum

end;

hence e in ee by A1; :: thesis: verum

end;

suppose A13: e = {2,3} ; :: thesis: b₁ in ee

now :: thesis: ex i, j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )

take i = 2; :: thesis: ex j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
take j = 3; :: thesis: ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
thus ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j ) by A13; :: thesis: verum

end;

hence e in ee by A1; :: thesis: verum

end;

suppose A14: e = {3,1} ; :: thesis: b₁ in ee

now :: thesis: ex i, j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )

take i = 3; :: thesis: ex j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
take j = 1; :: thesis: ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
thus ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j ) by A14; :: thesis: verum

end;

hence e in ee by A1; :: thesis: verum

end;

end;

end;

then {.{.1,2.},{.2,3.},{.3,1.}.} c= ee ;
hence ( ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) ) by A2, A10, XBOOLE_0:def 10; :: thesis: verum