theorem Th23: :: SGRAPH1:23

for X being set
for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for n being set
for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X