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