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