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
; ( ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) )
now for a being object st a in ee holds
a in {.{.1,2.},{.2,3.},{.3,1.}.}let a be
object ;
( a in ee implies b1 in {.{.1,2.},{.2,3.},{.3,1.}.} )assume
a in ee
;
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;
end;
then A10:
ee c= {.{.1,2.},{.2,3.},{.3,1.}.}
;
now for e being object st e in {.{.1,2.},{.2,3.},{.3,1.}.} holds
e in eelet e be
object ;
( e in {.{.1,2.},{.2,3.},{.3,1.}.} implies b1 in ee )assume A11:
e in {.{.1,2.},{.2,3.},{.3,1.}.}
;
b1 in ee 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; verum