set EE = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } ;

now :: thesis: for e being object st e in { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } holds
e in TWOELEMENTSETS (Seg n)

let e be object ; :: thesis: ( e in { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } implies e in TWOELEMENTSETS (Seg n) )
reconsider ee = e as set by TARSKI:1;
assume e in { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } ; :: thesis: e in TWOELEMENTSETS (Seg n)
then consider i0, j0 being Element of NAT such that
A1: e = {i0,j0} and
A2: i0 in Seg n and
A3: j0 in Seg n and
A4: i0 <> j0 ;
ee c= Seg n

proof

let e0 be object ; :: according to TARSKI:def 3 :: thesis: ( not e0 in ee or e0 in Seg n )
assume A5: e0 in ee ; :: thesis: e0 in Seg n

per cases ( e0 = i0 or e0 = j0 ) by A1, A5, TARSKI:def 2;

suppose e0 = i0 ; :: thesis: e0 in Seg n

hence e0 in Seg n by A2; :: thesis: verum

end;

suppose e0 = j0 ; :: thesis: e0 in Seg n

hence e0 in Seg n by A3; :: thesis: verum

end;

end;

end;

hence e in TWOELEMENTSETS (Seg n) by A1, A2, A3, A4, Th8; :: thesis: verum

end;

then { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } c= TWOELEMENTSETS (Seg n) ;
then reconsider EE = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } as finite Subset of (TWOELEMENTSETS (Seg n)) ;
set IT = SimpleGraphStruct(# (Seg n),EE #);
SimpleGraphStruct(# (Seg n),EE #) in SIMPLEGRAPHS NAT ;
then reconsider IT = SimpleGraphStruct(# (Seg n),EE #) as SimpleGraph of NAT by Def4;
take IT ; :: thesis: ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st
( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & IT = SimpleGraphStruct(# (Seg n),ee #) )
take EE ; :: thesis: ( EE = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & IT = SimpleGraphStruct(# (Seg n),EE #) )
thus ( EE = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & IT = SimpleGraphStruct(# (Seg n),EE #) ) ; :: thesis: verum