theorem Th16: :: SGRAPH1:16

for X being set holds SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in SIMPLEGRAPHS X