let G1, G2 be _Graph; :: thesis: ( {G1,G2} is vertex-disjoint iff ( G1 = G2 or the_Vertices_of G1 misses the_Vertices_of G2 ) )

hereby :: thesis: ( ( G1 = G2 or the_Vertices_of G1 misses the_Vertices_of G2 ) implies {G1,G2} is vertex-disjoint )

assume A1: {G1,G2} is vertex-disjoint ; :: thesis: ( G1 <> G2 implies the_Vertices_of G1 misses the_Vertices_of G2 )
assume A2: G1 <> G2 ; :: thesis: the_Vertices_of G1 misses the_Vertices_of G2
( G1 in {G1,G2} & G2 in {G1,G2} ) by TARSKI:def 2;
hence the_Vertices_of G1 misses the_Vertices_of G2 by A1, A2; :: thesis: verum

end;

assume ( G1 = G2 or the_Vertices_of G1 misses the_Vertices_of G2 ) ; :: thesis: {G1,G2} is vertex-disjoint

per cases then ( G1 = G2 or the_Vertices_of G1 misses the_Vertices_of G2 ) ;

suppose G1 = G2 ; :: thesis: {G1,G2} is vertex-disjoint

then {G1,G2} = {G1} by ENUMSET1:29;
hence {G1,G2} is vertex-disjoint ; :: thesis: verum

end;

suppose A3: the_Vertices_of G1 misses the_Vertices_of G2 ; :: thesis: {G1,G2} is vertex-disjoint

let G3, G4 be _Graph; :: according to GLIB_015:def 18 :: thesis: ( G3 in {G1,G2} & G4 in {G1,G2} & G3 <> G4 implies the_Vertices_of G3 misses the_Vertices_of G4 )
assume ( G3 in {G1,G2} & G4 in {G1,G2} & G3 <> G4 ) ; :: thesis: the_Vertices_of G3 misses the_Vertices_of G4
then ( ( G3 = G1 or G3 = G2 ) & ( G4 = G1 or G4 = G2 ) & G3 <> G4 ) by TARSKI:def 2;
hence the_Vertices_of G3 misses the_Vertices_of G4 by A3; :: thesis: verum

end;

end;