let G1, G2 be _Graph; :: thesis: ( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) iff {G1,G2} is /\-tolerating )
hereby :: thesis: ( {G1,G2} is /\-tolerating implies ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) )
assume A1: ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) ; :: thesis: {G1,G2} is /\-tolerating
then (the_Vertices_of G1) /\ (the_Vertices_of G2) <> {} by XBOOLE_0:def 7;
then meet {(the_Vertices_of G1),(the_Vertices_of G2)} <> {} by SETFAM_1:11;
then A2: meet (the_Vertices_of {G1,G2}) <> {} by Th6;
{G1,G2} is \/-tolerating by A1, Th19;
hence {G1,G2} is /\-tolerating by A2; :: thesis: verum
end;
assume A3: {G1,G2} is /\-tolerating ; :: thesis: ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 )
hence G1 tolerates G2 by Th19; :: thesis: the_Vertices_of G1 meets the_Vertices_of G2
meet {(the_Vertices_of G1),(the_Vertices_of G2)} <> {} by A3, Th6;
then (the_Vertices_of G1) /\ (the_Vertices_of G2) <> {} by SETFAM_1:11;
hence the_Vertices_of G1 meets the_Vertices_of G2 by XBOOLE_0:def 7; :: thesis: verum