for X, A being set st A is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS X c= A