let X be set ; :: thesis: for g being SimpleGraph of X holds
( g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) or ex v being set ex e being Subset of (TWOELEMENTSETS v) st
( not v is empty & g = SimpleGraphStruct(# v,e #) ) )
let g be SimpleGraph of X; :: thesis: ( g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) or ex v being set ex e being Subset of (TWOELEMENTSETS v) st
( not v is empty & g = SimpleGraphStruct(# v,e #) ) )
assume A1: not g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) ; :: thesis: ex v being set ex e being Subset of (TWOELEMENTSETS v) st
( not v is empty & g = SimpleGraphStruct(# v,e #) )
take the carrier of g ; :: thesis: ex e being Subset of (TWOELEMENTSETS the carrier of g) st
( not the carrier of g is empty & g = SimpleGraphStruct(# the carrier of g,e #) )
take the SEdges of g ; :: thesis: ( not the carrier of g is empty & g = SimpleGraphStruct(# the carrier of g, the SEdges of g #) )
thus not the carrier of g is empty by A1, Th13; :: thesis: g = SimpleGraphStruct(# the carrier of g, the SEdges of g #)
thus g = SimpleGraphStruct(# the carrier of g, the SEdges of g #) ; :: thesis: verum