let G1, G2 be _Graph; :: thesis: ( <*G1,G2*> is vertex-disjoint iff the_Vertices_of G1 misses the_Vertices_of G2 )
set F = <*G1,G2*>;

hereby :: thesis: ( the_Vertices_of G1 misses the_Vertices_of G2 implies <*G1,G2*> is vertex-disjoint )

assume A1: <*G1,G2*> is vertex-disjoint ; :: thesis: the_Vertices_of G1 misses the_Vertices_of G2
( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def 2;
then reconsider x1 = 1, x2 = 2 as Element of dom <*G1,G2*> by FINSEQ_1:92;
the_Vertices_of (<*G1,G2*> . x1) misses the_Vertices_of (<*G1,G2*> . x2) by A1;
then the_Vertices_of G1 misses the_Vertices_of (<*G1,G2*> . x2) ;
hence the_Vertices_of G1 misses the_Vertices_of G2 ; :: thesis: verum

end;

assume A2: the_Vertices_of G1 misses the_Vertices_of G2 ; :: thesis: <*G1,G2*> is vertex-disjoint
let x1, x2 be Element of dom <*G1,G2*>; :: according to GLIB_015:def 22 :: thesis: ( x1 <> x2 implies the_Vertices_of (<*G1,G2*> . x1) misses the_Vertices_of (<*G1,G2*> . x2) )
assume A3: x1 <> x2 ; :: thesis: the_Vertices_of (<*G1,G2*> . x1) misses the_Vertices_of (<*G1,G2*> . x2)
( x1 in dom <*G1,G2*> & x2 in dom <*G1,G2*> ) ;
then ( x1 in {1,2} & x2 in {1,2} ) by FINSEQ_1:92;
then ( ( x1 = 1 or x1 = 2 ) & ( x2 = 1 or x2 = 2 ) ) by TARSKI:def 2;

per cases then ( ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) ) by A3;

suppose ( x1 = 1 & x2 = 2 ) ; :: thesis: the_Vertices_of (<*G1,G2*> . x1) misses the_Vertices_of (<*G1,G2*> . x2)

then ( <*G1,G2*> . x1 = G1 & <*G1,G2*> . x2 = G2 ) ;
hence the_Vertices_of (<*G1,G2*> . x1) misses the_Vertices_of (<*G1,G2*> . x2) by A2; :: thesis: verum

end;

suppose ( x1 = 2 & x2 = 1 ) ; :: thesis: the_Vertices_of (<*G1,G2*> . x1) misses the_Vertices_of (<*G1,G2*> . x2)

then ( <*G1,G2*> . x2 = G1 & <*G1,G2*> . x1 = G2 ) ;
hence the_Vertices_of (<*G1,G2*> . x1) misses the_Vertices_of (<*G1,G2*> . x2) by A2; :: thesis: verum

end;

end;