let X be set ; :: thesis: SimpleGraphStruct(# {} ,({} (TWOELEMENTSETS {} )) #) in SIMPLEGRAPHS X
reconsider phiv = {} as finite Subset of by XBOOLE_1:2;
reconsider phie = {} (TWOELEMENTSETS {} ) as finite Subset of ;
SimpleGraphStruct(# phiv,phie #) in { SimpleGraphStruct(# v,e #) where v is finite Subset of , e is finite Subset of : verum } ;
hence SimpleGraphStruct(# {} ,({} (TWOELEMENTSETS {} )) #) in SIMPLEGRAPHS X ; :: thesis: verum