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