let G1, G2 be _Graph; :: thesis: for G being GraphMeet of G1,G2 st the_Vertices_of G1 meets the_Vertices_of G2 & the_Edges_of G1 misses the_Edges_of G2 holds
G is edgeless
let G be GraphMeet of G1,G2; :: thesis: ( the_Vertices_of G1 meets the_Vertices_of G2 & the_Edges_of G1 misses the_Edges_of G2 implies G is edgeless )
assume that
A1: the_Vertices_of G1 meets the_Vertices_of G2 and
A2: the_Edges_of G1 misses the_Edges_of G2 ; :: thesis: G is edgeless
G1 tolerates G2 by A2, Th12;
then the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) by A1, Th40
.= {} by A2, XBOOLE_0:def 7 ;
hence G is edgeless ; :: thesis: verum