let S be Graph-membered set ; :: thesis: ( S is edgeless implies S is edge-disjoint )
assume A1: S is edgeless ; :: thesis: S is edge-disjoint
let G1, G2 be _Graph; :: according to GLIB_015:def 19 :: thesis: ( G1 in S & G2 in S & G1 <> G2 implies the_Edges_of G1 misses the_Edges_of G2 )
assume ( G1 in S & G2 in S & G1 <> G2 ) ; :: thesis: the_Edges_of G1 misses the_Edges_of G2
then ( the_Edges_of G1 = {} & the_Edges_of G2 = {} ) by A1;
hence the_Edges_of G1 misses the_Edges_of G2 by XBOOLE_1:65; :: thesis: verum