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