set VV = Seg (m + n);
set V1 = Seg m;
set V2 = nat_interval ((m + 1),(m + n));
set EE = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } ;
A1: Seg m c= Seg (m + n) by FINSEQ_1:5, NAT_1:11;
A2: nat_interval ((m + 1),(m + n)) c= Seg (m + n) by Th4, NAT_1:11;
{ {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } c= TWOELEMENTSETS (Seg (m + n))

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } or e in TWOELEMENTSETS (Seg (m + n)) )
reconsider ee = e as set by TARSKI:1;
assume e in { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } ; :: thesis: e in TWOELEMENTSETS (Seg (m + n))
then consider i0, j0 being Element of NAT such that
A3: e = {i0,j0} and
A4: ( i0 in Seg m & j0 in nat_interval ((m + 1),(m + n)) ) ;
( i0 in Seg (m + n) & j0 in Seg (m + n) ) by A1, A2, A4;
then A5: ee c= Seg (m + n) by A3, TARSKI:def 2;
m < m + 1 by NAT_1:13;
then (Seg m) /\ (nat_interval ((m + 1),(m + n))) = {} by XBOOLE_0:def 7, Th5;
then i0 <> j0 by A4, XBOOLE_0:def 4;
hence e in TWOELEMENTSETS (Seg (m + n)) by A1, A2, A3, A4, A5, Th8; :: thesis: verum

end;

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