take SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) ; :: thesis: SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) is Element of SIMPLEGRAPHS X
thus SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) is Element of SIMPLEGRAPHS X by Th16; :: thesis: verum