begin
Lm1:
for e being set
for n being Element of NAT st e in Seg n holds
ex i being Element of NAT st
( e = i & 1 <= i & i <= n )
Lm2:
for A being set
for s being Subset of A
for n being set st n in A holds
s \/ {n} is Subset of A
begin
begin
begin
scheme
IndSimpleGraphs0{
F1()
-> set ,
P1[
set ] } :
provided
begin
begin
begin
begin
definition
let n,
m be
Element of
NAT ;
existence
ex b1 being SimpleGraph of NAT 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)) ) } & b1 = SimpleGraphStruct(# (Seg (m + n)),ee #) )
uniqueness
for b1, b2 being SimpleGraph of NAT st 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)) ) } & b1 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) & 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)) ) } & b2 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) holds
b1 = b2
;
end;
definition
let n be
Element of
NAT ;
existence
ex b1 being SimpleGraph of NAT 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 ) } & b1 = SimpleGraphStruct(# (Seg n),ee #) )
uniqueness
for b1, b2 being SimpleGraph of NAT st 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 ) } & b1 = SimpleGraphStruct(# (Seg n),ee #) ) & 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 ) } & b2 = SimpleGraphStruct(# (Seg n),ee #) ) holds
b1 = b2
;
end;
:: so we use a symbol nat_interval here.
:: following the definition of Seg, I add an assumption 1 <= m.
:: but it is unnatural, I think.
:: I changed the proof of existence
:: so that the assumption (1 <= m) is not necessary.
:: now nat_interval has the very natural definition, I think (-: