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 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 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 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 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 implies SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X )
set g = SimpleGraphStruct(# V,E #);
assume that
A1: SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X and
A2: n in X ; :: thesis: SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
reconsider g = SimpleGraphStruct(# V,E #) as SimpleGraph of X by A1, Def4;
V = the carrier of g ;
then V is finite Subset of X by Th21;
then V \/ {n} is finite Subset of X by A2, Lm1;
hence SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X ; :: thesis: verum