theorem Th25: :: SGRAPH1:25

for X being set holds SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X by Th16, Th23, Th24;