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