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