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 b1 in {.{.1,2.},{.2,3.},{.3,1.}.} )
assume a in ee ; :: thesis: b1 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;
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 b1 in ee )
assume A11: e in {.{.1,2.},{.2,3.},{.3,1.}.} ; :: thesis: b1 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: b1 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: b1 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: b1 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