let X be set ; :: thesis: SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X
thus SimpleGraphStruct(# {} ,({} (TWOELEMENTSETS {} )) #) in SIMPLEGRAPHS X by Th19; :: according to SGRAPH1:def 9 :: 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 & not n in V holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X ) & ( for V being Subset of
for E being Subset of
for v1, v2 being set st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & v1 in V & v2 in V & v1 <> v2 & not {v1,v2} in E holds
ex v1v2 being finite Subset of st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X ) ) )
thus for VV being Subset of
for EE being Subset of
for nn being set
for EEvn being finite Subset of st SimpleGraphStruct(# VV,EE #) in SIMPLEGRAPHS X & nn in X & not nn in VV holds
SimpleGraphStruct(# (VV \/ {nn}),EEvn #) in SIMPLEGRAPHS X by Th30; :: thesis: for V being Subset of
for E being Subset of
for v1, v2 being set st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & v1 in V & v2 in V & v1 <> v2 & not {v1,v2} in E holds
ex v1v2 being finite Subset of st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
thus for V being Subset of
for E being Subset of
for v1, v2 being set st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & v1 in V & v2 in V & v1 <> v2 & not {v1,v2} in E holds
ex v1v2 being finite Subset of st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X ) by Th31; :: thesis: verum