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