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 ;
TARSKI:def 3 ( 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)) ) }
;
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;
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
; 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
; ( 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 #) )
; verum