let G1 be non _trivial _Graph; :: thesis: for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
not v2 is isolated
let G2 be GraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
not v2 is isolated
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
not v2 is isolated
let v2 be Vertex of G2; :: thesis: ( v1 = v2 & v1 is isolated implies not v2 is isolated )
assume A1: v1 = v2 ; :: thesis: ( not v1 is isolated or not v2 is isolated )
assume A2: v1 is isolated ; :: thesis: not v2 is isolated
set v9 = the Element of (the_Vertices_of G1) \ {v1};
(the_Vertices_of G1) \ {v1} <> {} by GLIB_000:20;
then A3: the Element of (the_Vertices_of G1) \ {v1} in (the_Vertices_of G1) \ {v1} ;
then reconsider v9 = the Element of (the_Vertices_of G1) \ {v1} as Vertex of G1 ;
A4: v9 <> v1 by A3, ZFMISC_1:56;
for e being object holds not e Joins v1,v9,G1 by A2, GLIB_000:143;
then ex e being object st e Joins v1,v9,G2 by A4, Th98;
hence not v2 is isolated by A1, GLIB_000:143; :: thesis: verum