for X being set holds
( SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X & ( for A being set st A is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS X c= A ) ) by Th25, Th26;