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