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 ) } & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) ) by Def17;
take ee ; :: thesis: ( ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) )

now

let a be set ; :: 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
A2: ( a = {i,j} & i in Seg 3 & j in Seg 3 & i <> j ) by A1;

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

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

now

per cases ( j = 1 or j = 2 or j = 3 ) by A2, 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 A2, A3; :: 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 A2, A3, 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 A2, A3, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

now

per cases ( j = 1 or j = 2 or j = 3 ) by A2, 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 A2, A4, 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 A2, A4; :: 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 A2, A4, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

now

per cases ( j = 1 or j = 2 or j = 3 ) by A2, 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 A2, A5, 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 A2, A5, 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 A2, A5; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

then A6: ee c= {.{.1,2.},{.2,3.},{.3,1.}.} by TARSKI:def 3;

now

let e be set ; :: thesis: ( e in {.{.1,2.},{.2,3.},{.3,1.}.} implies b₁ in ee )
assume A7: 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 A7, ENUMSET1:def 1;

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

now

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 A8; :: thesis: ( i in Seg 3 & j in Seg 3 & i <> j )
thus ( i in Seg 3 & j in Seg 3 ) by ENUMSET1:def 1, FINSEQ_3:1; :: thesis: i <> j
thus i <> j ; :: thesis: verum

end;

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

end;

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

now

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 A9, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

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

end;

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

now

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 A10, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

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

end;

end;

end;

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