let X be set ; :: thesis: for g being SimpleGraph of X holds
( the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS the carrier of g )
let g be SimpleGraph of X; :: thesis: ( the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS the carrier of g )
g is Element of SIMPLEGRAPHS X by Def4;
then ex v being finite Subset of X ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) by Th17;
hence the carrier of g c= X ; :: thesis: the SEdges of g c= TWOELEMENTSETS the carrier of g
thus the SEdges of g c= TWOELEMENTSETS the carrier of g ; :: thesis: verum