let X be set ; :: thesis: 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 & not n in V holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
let V be Subset of X; :: thesis: 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 & not n in V holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
let E be Subset of (TWOELEMENTSETS V); :: thesis: for n being set
for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X & not n in V holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
let n be set ; :: thesis: for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X & not n in V holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
let Evn be finite Subset of (TWOELEMENTSETS (V \/ {n})); :: thesis: ( SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X & not n in V implies SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X )
set g = SimpleGraphStruct(# V,E #);
assume A1: ( SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X & not n in V ) ; :: thesis: SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
then reconsider g = SimpleGraphStruct(# V,E #) as SimpleGraph of X by Def7;
V = the carrier of g ;
then V is finite Subset of X by Th27;
then V \/ {n} is finite Subset of X by A1, Lm2;
hence SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X ; :: thesis: verum